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