Customer Reviews

Symbolic Logic and Mechanical Theorem Proving (Computer Science and Applied Mathematics)

5 star:		(4)
4 star:		(0)
3 star:		(0)
2 star:		(0)
1 star:		(0)

 

 

Best introductory book on automated theorem proving available. Although it was written in the early 70's, it is written in a very clear, but mathematically precise, manner. It does not drown a reader with an abundance of symbols and definitions. It is a clear and well written exposition on automated theorem proving based on resolution. Unlike some recent text books, it does NOT use sequentzen logic systems. It covers all aspects of resolution-based theorem proving: different forms of resolution, deletion strategies, unification.

If you are interested in Artificial Intelligence or you are one of those crazy guys who likes the Computer theory area this is a good book for you, mechanical theorem proving is an important subject into the AI area, all you want to know is Mathematical Logic, first order logic and predicate calculus. Very good book but very hard too (specially if you have to make some Mechanical theorem provers by yourself as a school project :) )

This book provides a complete introduction to mechanical theorem proving, including a lesson in both predicate calculus and first order logic. It is also profoundly readable.

Each concept is presented intuitively, abstractly (rigorously), then practically. Every technique and virtually every definition is proceeded by an example in both predicate calculus and first order logic, the first to show its simplicity, and the second to show its power. Proofs of the validity and completeness of every technique are provided to satisfy any concerns about them (and to interest theorists), but are not essential for comprehension of the book. Furthermore, the algorithms are all presented in a mathematically rigorous way, yet in a way that is quickly implemented on a computer.

In short, this book contains everything you need, whether you are interested in the subject or actually want/need to build a theorem prover. Furthermore, it's made as easy as the concepts can possibly be, and very rarely do you have to re-read a section to understand. This is the perfect book on the subject.

If you're a beginner who wants to build a FOL theorem prover, this is the first book you must get. The exposition is exemplary in clarity.

Though published in 1973, the material is not outdated. Many newer books talk about essentially the same basics, only harder to read.

It also explains answer extraction (ie, how to answer "what", "where", "when", "who" questions via resolution and unification).