Popular repositories Loading

1. logic-theorist logic-theorist Public

   The sources of the first theorem prover.

   62 7

2. theoremprover-museum.github.io theoremprover-museum.github.io Public

   HTML 56 7

3. LCF77 LCF77 Public

   The original Edinburgh LCF.

   Common Lisp 32 2

4. prover9 prover9 Public

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

   C 16 3

5. HOL88 HOL88 Public

   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 10 2

6. OMEGA OMEGA Public

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

   Isabelle 8