Metamathematics, Machines and Godel's Proof

Cambridge, MA.: Cambridge University Press , 1994. Text deals with the interactions between logic and computing, primarily how computers can be used to construct and check mathematical proofs. Describes the use of the Boyer-Moore theorem prover in verifying proofs of Godel's first incompleteness theorem, the Church-Rosser theorem of the lambda calculus, etc. he computer verification using the Boyer-Moore theorem prover… Ler mais sobre este item

Cambridge University Press, 1997-01-01. Paperback. New. New. In shrink wrap. Looks like an interesting title!