Math Logic and Foundations Software

• ACL2 Version 2.9  - Computational Logic Applicative Common Lisp. Models computer systems and proves properties of those models. With links to tours and demos, and software download.
• Church  - Allows simple experimentation with the lambda calculus, first developed by Church. To be used as a module imported by Python programs.
• Gateway to Logic  - Collection of interactive logic software that can be useful in lectures and courses for demonstration and visualization.
• Isabelle  - Generic proof assistant that allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Available for download.
• Linear Logic Prover (llprover)  - Searches a cut-free proof of the given two-sided sequent of first-order linear logic. With links to the prover program and whole package, user's guide, and related links.
• Logic Software from CSLI  - Software packages include Hyperproof, The Language of First-order Logic, Tarski's World and Turing's World. Published by the Center for the Study of Language and Information.
• Logics Workbench  - Offers possibility to work in a user-friendly way in classical and non-classical propositional logics, including nonmonotonic approaches. Developed at the University of Bern in Switzerland.
• LOOM  - Knowledge representation language developed by researchers in the Artificial Intelligence research group at the University of Southern California's Information Sciences Institute. With links to download software.
• MUltlog  - Project of the Vienna Group for Multiple-valued Logics. Available for free download.
• MUltseq  - Companion for MUltlog. Uses rules from Multlog to construct derivations - automatically or interactively - for sequents given directly by the user or generated from the (quasi-) equations.
• Proof General  - Generic interface for proof assistants, based on the customizable text editor Emacs.
• ProofPower  - Supports specification and proof in Higher Order Logic (HOL) and in the Z notation. All packages, except PPDaz, are free, open-source, software made available under the terms of the GNU General Public License.
• PVS Specification and Verification System  - Specification language integrated with support tools and a theorem prover. With documentation and download links.
• Tree Proof Generator (Semantic Tableaux)  - Generates tableaux for classical propositional and predicate logic.
• VeriFun  - Java application to verify functional programs. With link to download program.