The Theorem Prover Museum - Museum

The Theorem Prover Museum

Theorem provers are software systems that can find or check proofs for conjectures given in some logic. Research in theorem proving system started with the logical theorist 1955 and has led to a succession of systems since.

Theorem provers are complex software systems that have pushed the envelope of artificial intelligence and programming, and as such they constitute important cultural artifacts.

With the current wave of retirements of the original principal investigators there is good chance that the systems are lost, when their group servers are shut down. This web site aims to preserve the ones we can still get our hands on. This idea is compatible with the Software Heritage initiative, and contributes since it is based on GitHub repositories.

The term “museum” may be sound bit ambitious, since the exhibition and didactic interpretation of the theorem provers is beyond our scope (and perhaps abilities). But the foremost function of a museum is the conservation of artifacts, which is what the “theorem prover museum” project intends to do.

This site is the front-end to a collection of source code repositories for theorem provers (see below). To exhibit your system here or suggest a system for inclusion (most wanted list, systems believed lost), please contact Michael Kohlhase. See also Contributors, Community, project/issues.

Note that it is not the purpose of this site to keep the theorem proving systems running (in many cases the compilers and dependencies have moved on, making this very difficult), but only to archive the source code for academic study. In particular this should lower the barrier of archiving systems here.

Latest News Full List atom feed

Theorem Prover Museum has news
22 September 2017

swMATH links
9 September 2017

The sources of the first theorem prover (Logic Theorist) found!
2 September 2017

Theorem Prover Museum has 20 Provers
7 April 2017

Theorem Prover Museum has 10 Provers
10 December 2016

Encyclopedia of proof systems, Wikipedia page, … more.

All theorem provers start out as active systems, eventually development gets discontinued as developers retire or move to newer systems. Therefore we also maintain a list of source code repositories of active theorem provers.

IMPS

The IMPS Theorem Prover.

MKRP

The Markgraph Karl Refutation Procedure, a graph-based resolution theorem prover written in Common Lisp

OMEGA

A theorem prover for higher-order logic based on proof planning.

InKa

An Inductive Theorem Prover

Otter

The first theorem prover for first-order logic with equality from the Argonne group that was widely distributed.

Mace

The Argonne Model generator.

Prover9

Prover9 is the successor to Otter

Mace4

Mace4 is the successor of Mace.

PRESS

The Prolog Equation Solving System (PRESS) pioneered work on what is now called proof planning.

LCF77

The original Edinburgh LCF

TPS

TPS is an interactive, semi-automatic, and automatic Theorem Proving System for first-order logic and higher-order logic. The subsystem ETPS is designed for interactive use by students in logic courses.

HOL88

The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML.

HOL90

The rational reconstruction of HOL88

SNARK

SRI's New Automated Reasoning Kit

PRV

PRV-Beweisprogramm really: an early theorem prover written in SNOBOL

OSHL

A general-purpose instance-based first-order automated theorem proving algorithm

CLIN

A Semantically Guided First-Order Theorem Prover

NQTHM

An improved version of the original Boyer-Moore theorem prover

clam2

A Prolog implementation of the proof planner Clam (in the clam2 development branch) and the associated theorem prover, oyster.

Clam 3

Prolog implementation of proof planner with critics, and some higher-order unification, in the v3 branch of Clam.

LambdaClam

A proof planning system that support proof planning over higher-order domains.

MUSCADET

An automatic theorem proving system using knowledge and metaknowledge in mathematics.

DISCOUNT

A Distributed and Learning Equational Prover.

SAD

A tool for automated verification of formal mathematical texts.

scunac

A proof checker and interactive theorem prover for dependently typed set theory.

SETHEO

A first-order theorem prover based on the connection method.

ProCom

A theorem prover based on the PTTP paradigm.

Logic Theorist

The first theorem prover by Newell and Simon.