Repositories list

• theoremprover-museum.github.io

  Public
  HTML

  •

  GNU General Public License v3.0

  •7•51•16•0•Updated Aug 11, 2024Aug 11, 2024

• fellowship

  Public
  OCaml

  •0•0•0•0•Updated Aug 6, 2024Aug 6, 2024

• minlog

  Public
  0•0•0•0•Updated Aug 6, 2024Aug 6, 2024

• larch

  Public
  The Larch Theorem Prover from MIT

  0•0•0•0•Updated Jul 3, 2024Jul 3, 2024

• Ehdm

  Public
  The Ehdm theorem prover developed at SRI in the 80s.

  0•0•0•0•Updated Jun 22, 2024Jun 22, 2024

• egal

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

  theorem-provingverificationproof-assistant+ 3set-theoryhigher-order-logictheorem-prover

  OCaml

  •

  Other

  •0•2•0•0•Updated Jul 15, 2021Jul 15, 2021

• SEQUEL

  Public
  Mark Tarver's SEQUEL system versions 7.0 and 5.3

  HTML

  •0•0•0•0•Updated Jul 6, 2020Jul 6, 2020

• oleg

  Public archive
  Standard ML

  •1•1•0•0•Updated May 2, 2020May 2, 2020

• doc

  Public
  Documentation about the Theorem Prover Museum

  TeX

  •0•1•0•0•Updated Jun 11, 2019Jun 11, 2019

• muscadet

  Public
  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

  •

  Other

  •1•2•0•0•Updated Dec 7, 2018Dec 7, 2018

• Peers-mcd

  Public
  the Peers-mcd theorem provers

  C

  •0•0•0•0•Updated Sep 28, 2018Sep 28, 2018

• Peers

  Public
  The Peers Theorem Prover

  C

  •0•0•0•0•Updated Sep 18, 2018Sep 18, 2018

• Aquarius

  Public
  The Aquarius Theorem Prover

  C

  •0•0•0•0•Updated Sep 18, 2018Sep 18, 2018

• LEGO

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

  Lex

  •0•2•0•0•Updated Jun 21, 2018Jun 21, 2018

• isabelle

  Public
  Archival Versions of the Isabelle Theorem Prover

  0•0•0•0•Updated Jun 20, 2018Jun 20, 2018

• EQP

  Public
  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

  •1•5•0•0•Updated Jun 20, 2018Jun 20, 2018

• PLTP

  Public
  The Edinburgh Pure Lisp Theorem Prover (Boyer/Moore)

  HTML

  •0•0•0•0•Updated Jun 19, 2018Jun 19, 2018

• ClassInt

  Public
  C++

  •0•0•0•0•Updated Jun 19, 2018Jun 19, 2018

• RDL

  Public
  Rewrite and Decision Procedure Laboratory

  Prolog

  •0•0•0•0•Updated Jun 19, 2018Jun 19, 2018

• prover9

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

  C

  •3•16•0•0•Updated May 4, 2018May 4, 2018

• logic-theorist

  Public
  The sources of the first theorem prover.

  6•56•1•0•Updated Sep 2, 2017Sep 2, 2017

• SETHEO

  Public
  The SETHEO theorem prover (C version)

  C

  •1•3•0•0•Updated Jun 27, 2017Jun 27, 2017

• ProCom

  Public
  A theorem prover based on the PTTP paradigm.

  Prolog

  •0•1•0•0•Updated Jun 26, 2017Jun 26, 2017

• scunac

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

  Common Lisp

  •0•2•0•0•Updated May 16, 2017May 16, 2017

• SNARK

  Public
  SNARK - SRI's New Automated Reasoning Kit

  Common Lisp

  •

  Other

  •0•1•0•0•Updated Apr 7, 2017Apr 7, 2017

• discount

  Public
  the discount theorem prover

  C

  •0•0•0•0•Updated Apr 7, 2017Apr 7, 2017

• lambdaclam

  Public
  AMPL

  •0•2•0•0•Updated Apr 4, 2017Apr 4, 2017

• HOL90

  Public
  The source of hte HOL90 Theorem prover.

  Standard ML

  •0•3•0•0•Updated Mar 28, 2017Mar 28, 2017

• OSHL

  Public
  C++

  •1•0•0•0•Updated Jan 9, 2017Jan 9, 2017

• clam3

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

  Prolog

  •0•6•0•0•Updated Dec 30, 2016Dec 30, 2016