- 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.
- ARG Software
- Provides links to software developed by the Automated Reasoning Group from the Computer Sciences Laboratory of the Australian National University.
- Church
- Allows simple experimentation with the lambda calculus, first developed by Church. To be used as a module imported by Python programs.
- Coq Proof Assistant
- Proof management system, in which proof is mechanically checked by the machine. Provides links for download, documentation, standard library, user's contribution and related tools.
- DELORES- Defeasible Logic Reasoning System
- Forward-chaining reasoning engine for defeasible logic. Distributed as C source code.
- 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.
- Paradox
- Processes first-order logic problems and tries to find finite-domain models for them. With link to download program.
- 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.
- Protein - PROver with a Theory Extension Interface
- Automated theorem prover for first-order clause logic. Available for free download.
- 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.
- WinKE: Proof Assistant for Teaching Logic
- Based on the KE calculus, a refutation system combining features from Smullyan's analytic tableaux and Gentzen's natural deduction. With information on how to download freeware.
|