Lean theorem prover

From Wikipedia, the free encyclopedia

A lean theorem prover is an automated theorem prover implemented in a minimum amount of code. Lean provers are generally^{[citation needed]} implemented in Prolog, and make proficient use of the backtracking engine and logic variables of that language. Lean provers can be as small as a few hundred bytes of source code.

[edit] Lean theorem provers

• leanCoP, a prover for classical first-order logic in 333 bytes
• leanTAP