Lean theorem prover

Lean theorem prover

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

* [http://www.leancop.de/ leanCoP] , a prover for classical first-order logic in 333 bytes
* [http://i12www.ira.uka.de/leantap/ leanTAP]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”