ONCE IT WAS ESTABLISHED that automated proof was not keeping all its promises, mathematicians conceived a less ambitious project, namely that of proof checking. When one uses an automated theorem proving program, one enters a proposition and the program attempts to construct a proof of the proposition. On the other hand, when one uses a proof-checking program, one enters both a proposition and a presumed proof of it and the program merely verifies the proof, checking it for correctness.

Although proof checking seems less ambitious than automated proof, it has been applied to more complex demonstrations and especially to real mathematical proofs. Thus, a large share of the first-year undergraduate mathematics syllabus ...

Start Free Trial

No credit card required