|
| Login | Sign up | My Wish List |
![]() | Automated Theorem Proving: Theory and Practice by Monty Newborn ISBN-10: 9780387950754 ISBN-10: 0-387-95075-3 ISBN-13: 9780387950754 ISBN-13: 978-0-387-95075-4 Hardcover 2000-12-15 Springer Find Lowest Price | |
Editorials | ||
Product Description This text and software package introduces the reader to automated theorem proving and provides two approaches implemented as easy-to-use programs. The two approaches studied are semantic tree theorem proving and resolution-refutation theorem proving. The first chapters introduce the reader to first-order predicate calculus, well-formed formulae, and their transformation to clauses (implemented in a third program provided on diskette). Then the author shows how the two methods work and provides numerous examples for readers to try their hand at theorem-proving experiments. Each chapter comes with exercises intended to familiarise the readers with the ideas and with the software, and answers are provided to many of the problems. | ||
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). | ||