Lean theorem prover

A lean theorem prover is an automated theorem prover implemented in a minimum amount of code. Lean provers are generally 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.

Lean theorem provers

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

This article is issued from Wikipedia - version of the Friday, February 12, 2010. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.