theoremprover-museum/theoremprover-museum.github.io

1

logic-theorist

The sources of the first theorem prover.

55

2

LCF77

The original Edinburgh LCF.

Common Lisp

23

3

prover9

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.

C

15

4

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.

Standard ML

9

5

OMEGA

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

Isabelle

7

6

imps

The IMPS Theorem Prover

Perl 6

7

7

clam3

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

Prolog

6

8

EQP

EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search.

C

5

9

InKa

InKa - an inductive theorem prover

Common Lisp

4

10

otter

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

C

4

11

HOL90

The source of hte HOL90 Theorem prover.

Standard ML

3

12

MKRP

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

Common Lisp

3

13

SETHEO

The SETHEO theorem prover (C version)

C

3

14

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.

Common Lisp

3

15

LEGO

the source archive for LEGO: an interactive proof development system for various type theories

Lex

2

16

scunac

a proof checker and interactive theorem prover for dependently typed set theory

Common Lisp

2

17

lambdaclam

AMPL

2

18

egal

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory

OCaml

2

19

muscadet

The Muscadet Theorem Prover is a knowledge-based system. Based on natural deduction, it uses methods which resemble those used by humans, implemented in one or several bases of facts. The output is an easily readable proof.

Prolog

2

20

SNARK

SNARK - SRI's New Automated Reasoning Kit

Common Lisp

1

21

ProCom

A theorem prover based on the PTTP paradigm.

Prolog

1

22

doc

Documentation about the Theorem Prover Museum

TeX

1

23

oleg

Standard ML

1

24

clam2

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

Prolog

1