Math Computational Logic in the Best of the Web Directory

Math Computational Logic


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.


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.


Generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).


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.


Proof-assistant for Pure Type Systems (PTSs) with several extensions. With user guide, installation guide, tutorials and articles about Yarrow.

Submit a site to this category