GETFOL

GETFOL Interactive Theorem Prover. 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.