Date: Mon, 3 Oct 1994 19:03:28 +0100
From: GETFOL Manager <getfol@frege.mrg.dist.unige.it>
To: massacci@assi.dis.uniroma1.it, nirad@cs.uq.oz.au,
        schumann@informatik.tu-muenchen.de, musto@iei.pi.cnr.it,
        freitag@informatik.tu-muenchen.de, treur@cs.vu.nl,
        frankh@swi.psy.uva.nl, smaill@aisb.ed.ac.uk, agc@ai.leeds.ac.uk,
        staples@cs.uq.oz.au, kerber@cs.uni-sb.de, e_motta@vax4.open.ac.uk,
        ruess@informatik.uni-ulm.de, laublet@laforia.ibp.fr,
        goerz@informatik.uni-erlangen.de, w.jonker@ecrc.de, jfp@laforia.ibp.fr,
        grosof@watson.ibm.com
Cc: theorem-provers@mc.lcs.mit.edu, qed@mcs.anl.gov, mind@aisb.ed.ac.uk,
        indus@aisb.ed.ac.uk, nqthm-users@cli.com, info-hol@cs.uidaho.edu,
        isabelle-users@cl.cam.ac.uk, dreamers@aisb.ed.ac.uk, risks@csl.sri.COM,
        mrg@frege.mrg.dist.unige.it.October.3, 1994@frege.mrg.dist.unige.it


             *** ANNOUNCING A NEW RELEASE OF THE GETFOL SYSTEM ***

The Mechanized Reasoning Group is pleased to announce release 2.001 of the
GETFOL system.

  GETFOL is  an interactive  reasoning system running  on  top  of a  complete
  reimplementation of the FOL system  (FOL was itself  developed by Richard W.
  Weyhrauch). GETFOL  can be used in many  ways, for instance as a programming
  language for building intelligent systems, as  an interactive theorem prover
  for first order logic or as an environment for the study of the mathematical
  theory of computation.  

  GETFOL has  a first  order sorted  language,   theory and axiom  declaration
  commands,   multiple  proofs,   natural  deduction   inference  rules  (with
  extensions to deal  with sorts), equality  rules, conditional rules (termif,
  wffif), structural rules (weaken, contract),  deciders for propositional and
  predicate logic,  semantic and  syntactic simplification, multiple contexts,
  meta-reasoning.


CHANGES FROM PREVIOUS RELEASE

   * Complete re-implementation of the deciders
   * Minor improvements to the administration commands
   * Bug fixes



GETFOL 2.001 can be obtained via ftp from the following address:

    Network address: frege.mrg.dist.unige.it (130.251.7.2)
    Login:           ftp (anonymous)
    Passwd:          <your full e-mail address>
    Directory:       pub/GETFOL
    File:            GETFOL2.001.tar.Z

GETFOL2.001.tar.Z  is  a compressed,  tar file  containing the  source code
and the documentation needed to run the system.


NEXT RELEASE

    * backward reasoning integrated with forward reasoning
    * tactic language
    * definitions mechanism
    * emacs interface
    * export of proofs to LaTeX source code


DISTRIBUTION POLICY

    * GETFOL is not guaranteed in any way.  It is provided "as is",
      without express or implied warranty.  We accept no responsibility
      for any damage that may result from its use. GETFOL is purely an
      experimental program.
    * GETFOL is maintained by Fausto Giunchiglia as a service to
      researchers interested in logic based representation theory. We
      hope to contribute to the development, sharing and spreading of 
      new ideas.


SYSTEM REQUIREMENTS

  GETFOL is implemented in HGKM, a language built on top of Common Lisp.
  GETFOL has been  successfully compiled  with KCL  (Kyoto Common  Lisp), AKCL
  (Austin Kyoto Common Lisp) Version(1.623) and Lucid (version 3.0.0) on Unix.


----------------------------------------------------------------------------
    If you have comments, requests, suggestions, please send e-mail to:

                        getfol@frege.mrg.dist.unige.it