Automated Theorem Proving: Theory and Practice

by Monty Newborn

Book Overview

This text and software package introduces readers to automated theorem proving, while providing two approaches implemented as easy-to-use programs. These are semantic-tree theorem proving and resolution-refutation theorem proving. The early chapters introduce first-order predicate calculus, well-formed formulae, and their transformation to clauses. Then the author goes on to show how the two methods work and provides numerous examples for readers...

• Format: Paperback
• Language: English
• ISBN: 1461265193
• ISBN13: 9781461265191
• Release Date: May 2013
• Publisher: Springer
• Length: 231 Pages
• Weight: 0.78 lbs.
• Dimensions: 0.5" x 6.1" x 9.2"

Customer Reviews

Learn about automated theorem proving in one weekend

So you wanted to know how automated theorem proving algorithms work? This is a "hands on" book that tells you just that and gives you the sources of a program that implements these algorithms. The book is a cross between giving you theory and telling you about the included programs. As such it is a fast read and is great to learn the basic concepts. Its short comings are that you sometimes need to reread a paragraph a few times because it is written in a fairly terse style. The code is meant to work under unix but compiles and run well under windows visual C++ although one program does not work fully (COMPILE).