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 by anonymous ftp (IP address 130.251.7.2).
GETFOL2.001.tar.Z is a compressed tar file containing the source code and the documentation needed to run the system.
NEXT RELEASE will feature: backward reasoning integrated with forward reasoning, tactic language, definitions mechanism, emacs interface, export of proofs to LaTeX source code.
DISTRIBUTION POLICY:
SYSTEM REQUIREMENTS: GETFOL is implemented in HGKM, a language on top of Common Lisp. GETFOL has been successfully compiled with KCL (Kyoto Common Lisp), AKCL (Austin KCL) V(1.623) and Lucid (v. 3.0.0) on Unix.
If you have comments, requests, suggestions, please send e-mail to:
getfol@frege.mrg.dist.unige.it