."..the main purpose of this book is to describe how the Boyer-Moore theorem prover was used to mechanically verify two landmark theorems of mathematical logic, Godel's first incompleteness theorem and the Church-Rosser theorem of the lambda calculus..for specialized collections in artificial intelligence." D.V. Feldman, Choice
--This text refers to an out of print or unavailable edition of this title.
Now in paperback, this book describes the use of a computer program to check the proofs of several celebrated theorems in metamathematics including Gödel's incompleteness theorem and the Church-Rosser theorem. The computer verification using the Boyer-Moore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology.