HERBY

Automated theorem proving. Theory and practice. With CD-ROM. The subject of this book is the theoretical and practical support of one of the most interesting area in Artificial Intelligence: automated theorem proving. In particular, it is about how two programs (written in C, included in CD-ROM), HERBY and THEO, carry out this process. A third program, COMPILE (also included), first negates the conclusion and then translates the axioms and the negated conclusion to clauses. Running these programs is the subject of the Chapter 1. Chapter 2 explains how to write a theorem as a set of wffs and Chapter 3 how to use COMPILE for transforming wffs to clauses. HERBY and THEO use two inference procedures: binary resolution and binary factoring (Chapter 4). HERBY is a semantic-tree theorem-proving program (the theoretical foundations of semantic tree theorem proving are presented in Chapter 5) and THEO is a resolution-refutation theorem -proving program (the theoretical foundations for resolution-refutation theorem-proving are presented in Chapter 6). Chapters 7 and 8 describe HERBY and how to use it, chapters 9 and 10 parallel 7 and 8, but for THEO. The final chapter, 13, briefly examines two other automated theorem-proving programs, {it Gandalf} and {it Otter}. par In his past, the author was involved in the design of chess programs. The search techniques used in the programs of this book are very similar to those used in chess programs. Both programs in this book have participated in the Conference on Automated Deduction’s competitions. The sourse cod has evolved over a ten-year period. par The book, software and text, with almost two hundred theorems, can serve as instructional material for a course on theorem proving or AI at either the undergraduate or graduate level.