- Alfa
- Proof editor succeeding ALF, an editor for direct manipulation of proof objects in a logical framework based on Per Martin-LC6f's Type Theory. Free download available.
- Automated Reasoning
- Article from the Stanford Encyclopedia of Philosophy.
- Coq Proof Assistant
- Formal proof management system, based on a logical framework called Calculus of Inductive Constructions extended by a modular development system for theories. With links to download, documentation and related tools.
- CtCoq
- Provides a working environment for the Coq theorem prover. Developed at INRIA Sophia Antipolis.
- Dual Identity Combinators
- Provides an analysis of the effect of the identity combinators in dual systems. Written by Katalin Bimbó.
- HOL Project
- Automated proof system for higher order logic. Operates as an open source project with a BSD-style license allowing free use in commercial products.
- Isabelle
- Generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
- John's Lambda Calculus and Combinatory Logic Playground
- Includes links to paper available in pdf or postscript, and a java applet interpreting the simplest language.
- Kumo
- Web-based proof assistant for first order-hidden logic, using OBJ3 as a reduction engine. Also generates proof documentation for the web and supports distributed cooperative proving.
- Lambda Calculus
- Guide to lazy and strict versions of the lambda-calculus interpreter.
- LEGO Proof Assistant
- Interactive proof development system designed and implemented by Randy Pollack in Edinburgh.
- MetaPRL
- Logical framework defining and relating multiple logics, and a system implementation with support for interactive proof and automated reasoning. With download links, tutorials, user guide and developer guide.
- PhoX Proof Assistant
- Proof assistant that is eXtensible and is based on High Order logic. Includes links to download system and manual.
- PRL Project
- Focuses on implementing computational mathematics and providing logic-based tools that help automate programming.
- Proof General
- Generic interface for proof assistants, based on the customizable text editor Emacs. Works with either XEmacs or GNU Emacs.
- Yarrow
- Proof-assistant for Pure Type Systems (PTSs) with several extensions. With user guide, installation guide, tutorials and articles about Yarrow.
|