From owner-qed Mon Oct 3 13:27:56 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA19811 for qed-out; Mon, 3 Oct 1994 13:24:58 -0500 Received: from frege.mrg.dist.unige.it (frege.mrg.dist.unige.it [130.251.7.2]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id NAA19787 for ; Mon, 3 Oct 1994 13:24:03 -0500 Received: from skolem.mrg.dist.unige.it by frege.mrg.dist.unige.it with SMTP id AA10761 (5.65c/IDA-1.4.4 for ); Mon, 3 Oct 1994 19:03:28 +0100 Date: Mon, 3 Oct 1994 19:03:28 +0100 From: GETFOL Manager Message-Id: <199410031803.AA10761@frege.mrg.dist.unige.it> Received: by skolem.mrg.dist.unige.it (4.1/SMI-4.1) id AA02845; Mon, 3 Oct 94 19:01:59 +0100 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 Sender: owner-qed@mcs.anl.gov Precedence: bulk *** 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: 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