Authomated Theorem Proving - Theory And Practice

As the 21st century begins, the power of our new tool and partner, the computer, is increasing at an astonishing rate. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from facts, or abstractly, to prove theorems, the subject of this book. "Automated Theorem Proving" describes how this process is performed. It first introduces the mathematical language of predicate calculus and then discusses the basic inferencing rules of binary resolution and binary factoring. Using these rules, two theorem-proving systems are described. The first (HERBY) is based on constructing closed sematic trees, whereas the second (THEO) is based on the classic resolution-refutation approach. These programs are included on the accompanying CD-ROM, which includes their source code and runs on both Unix and Linux. Topics and features: clear, concise presentation of the fundamentals extensive end-of-chapter exercises, with solutions HERBY, an excellent and unique semantic-tree theorem-proving program THEO, a strong resolution-refutation theorem-proving program approximately 200 theorems included on the CD-ROM for experimentation The book and software are an excellent text/reference for advanced students, practitioners, and professionals in computer science, applied math, logical computation and artificial intelligence. Anyone with an interest in automated reasoning will find the book an essential guide and hands-on tool for learning about the theorem-proving process.