Explore @theoremprover-museum Open Source projects

@theoremprover-museum

theoremprover-museum

Stars
214
Global Org. Rank 38,898 (Top 13 %)
Registered over 8 years ago
Most used languages

Common Lisp
25.0 %

C
16.7 %

Prolog
16.7 %

Standard ML 12.5 %

AMPL 4.2 %

TeX
4.2 %

Isabelle 4.2 %

HTML
4.2 %

Lex 4.2 %

OCaml
4.2 %

Perl 6 4.2 %

logic-theorist

The sources of the first theorem prover.

theoremprover-museum.github.io

LCF77

The original Edinburgh LCF.

prover9

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

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.

OMEGA

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

imps

The IMPS Theorem Prover

clam3

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

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.

InKa

InKa - an inductive theorem prover

otter

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

HOL90

The source of hte HOL90 Theorem prover.

MKRP

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

SETHEO

The SETHEO theorem prover (C version)

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.

LEGO

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

scunac

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

lambdaclam

egal

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

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.

SNARK

SNARK - SRI's New Automated Reasoning Kit

ProCom

A theorem prover based on the PTTP paradigm.

doc

Documentation about the Theorem Prover Museum

oleg

clam2

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