## Metamathematics, Machines, and Goedel's Proof

The revised Index is in:

For Table of Contents, see

** Blurb: **
Mathematicians from Leibniz to Hilbert have sought to mechanize the
verification of mathematical proofs. Developments arising out of
Goedel's proof of his incompleteness theorem showed that no computer
program could automatically prove all and only the valid statements of
mathematics. In practice, however, there are a number of
sophisticated automated reasoning programs that are quite effective at
checking mathematical proofs.
This book describes the use of a computer program to check the proofs
of several celebrated theorems in metamathematics including Goedel'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. The
mechanization of metamathematics itself has important implications for
automated reasoning since metatheorems can be applied as labor-saving
devices to simplify proof construction. The book should be accessible
to scientists or philosophers with some knowledge of logic and
computing.
Order your copy now using ISBN
0-521-58533-3.
OR try
Amazon.