HERBY swMATH ID: 21545 Software Authors: Newborn, Monty Description: 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. Homepage: http://www.springer.com/de/book/9780387950754 Keywords: predicate calculus; inference procedures; semantic trees; resolution refutation proofs Related Software: OTTER; TPTP; TGTP; SETHEO; Gandalf; MARTE; DaProS; UMLsec; SysML; Uppaal; NuSMV; SPIN; PRISM; Aquarius; METEOR; PARTHENON; Peers-mcd; SPTHEO; Bliksem; DISCOUNT Cited in: 5 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Automated theorem proving. Theory and practice. With CD-ROM. Zbl 0963.68176Newborn, Monty 2001 Heuristics used by HERBY for semantic tree theorem proving. Zbl 0913.68190Yu, Qingxun; Almulla, Mohammed; Newborn, Monroe 1998 all top 5 Cited by 7 Authors 2 Almulla, Mohammed 2 Newborn, Monty 1 Hanna, Latif A.-M. 1 Kim, Choon Kyu 1 Newborn, Monroe M. 1 Wang, Zongyan 1 Yu, Qingxun Cited in 4 Serials 1 Journal of Automated Reasoning 1 International Journal of Computer Mathematics 1 Annals of Mathematics and Artificial Intelligence 1 Kuwait Journal of Science and Engineering Cited in 2 Fields 5 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year