Skip to content

@theoremprover-museum theoremprover-museum

Change the repository type filter

All

    Repositories list

    43 repositories

    • logic-theorist

      Public
      The sources of the first theorem prover.
      8•74•1•0•Updated Apr 19, 2026Apr 19, 2026

    • fellowship

      Public
      OCaml
      •
      GNU General Public License v3.0
      •2•1•0•0•Updated Jul 4, 2025Jul 4, 2025

    • theoremprover-museum.github.io

      Public
      HTML
      •
      GNU General Public License v3.0
      •7•56•16•1•Updated Apr 24, 2025Apr 24, 2025

    • TATL

      Public
      The ATL* logic reasoner TATL*
      logicatltableau
      logicatltableaureasoning
      OCaml
      •
      Apache License 2.0
      •1•0•0•0•Updated Dec 2, 2024Dec 2, 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
      theorem-provingverificationproof-assistantset-theoryhigher-order-logictheorem-prover
      OCaml
      •
      Other
      •1•4•0•0•Updated Jul 15, 2021Jul 15, 2021

    • SEQUEL

      Public
      Mark Tarver's SEQUEL system versions 7.0 and 5.3
      HTML
      •1•0•0•0•Updated Jul 6, 2020Jul 6, 2020

    • oleg

      Public archive
      Standard ML
      •2•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 …
      Prolog
      •
      Other
      •2•2•0•0•Updated Dec 7, 2018Dec 7, 2018

    • Peers-mcd

      Public
      the Peers-mcd theorem provers
      C
      •1•0•0•0•Updated Sep 28, 2018Sep 28, 2018

    • Peers

      Public
      The Peers Theorem Prover
      C
      •1•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
      •2•3•0•0•Updated Jun 21, 2018Jun 21, 2018

    • isabelle

      Public
      Archival Versions of the Isabelle Theorem Prover
      1•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…
      C
      •2•5•0•0•Updated Jun 20, 2018Jun 20, 2018

    • PLTP

      Public
      The Edinburgh Pure Lisp Theorem Prover (Boyer/Moore)
      HTML
      •1•1•0•0•Updated Jun 19, 2018Jun 19, 2018

    • ClassInt

      Public
      C++
      •1•0•0•0•Updated Jun 19, 2018Jun 19, 2018

    • RDL

      Public
      Rewrite and Decision Procedure Laboratory
      Prolog
      •1•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
      •4•16•0•0•Updated May 4, 2018May 4, 2018

    • SETHEO

      Public
      The SETHEO theorem prover (C version)
      C
      •2•3•0•0•Updated Jun 27, 2017Jun 27, 2017

    • ProCom

      Public
      A theorem prover based on the PTTP paradigm.
      Prolog
      •1•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
      •1•3•0•0•Updated May 16, 2017May 16, 2017

    • SNARK

      Public
      SNARK - SRI's New Automated Reasoning Kit
      Common Lisp
      •
      Other
      •1•2•0•0•Updated Apr 7, 2017Apr 7, 2017

    • discount

      Public
      the discount theorem prover
      C
      •1•0•0•0•Updated Apr 7, 2017Apr 7, 2017

    • lambdaclam

      Public
      AMPL
      •1•2•0•0•Updated Apr 4, 2017Apr 4, 2017

    • HOL90

      Public
      The source of hte HOL90 Theorem prover.
      Standard ML
      •1•3•0•0•Updated Mar 28, 2017Mar 28, 2017

    • OSHL

      Public
      C++
      •2•0•0•0•Updated Jan 9, 2017Jan 9, 2017
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.