Popular repositories Loading

1. logic-theorist logic-theorist Public

   The sources of the first theorem prover.

   55 6

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

   HTML 51 7

3. LCF77 LCF77 Public

   The original Edinburgh LCF.

   Common Lisp 23 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 9 2

6. OMEGA OMEGA Public

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

   Isabelle 8