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