Math Computational Logic

• 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.