HERBY
swMATH ID:  21545 
Software Authors:  Newborn, Monty 
Description:  Automated theorem proving. Theory and practice. With CDROM. 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 CDROM), 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 semantictree theoremproving program (the theoretical foundations of semantic tree theorem proving are presented in Chapter 5) and THEO is a resolutionrefutation theorem proving program (the theoretical foundations for resolutionrefutation theoremproving 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 theoremproving 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 tenyear 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; Peersmcd; 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 CDROM. Zbl 0963.68176 Newborn, Monty 
2001

Heuristics used by HERBY for semantic tree theorem proving. Zbl 0913.68190 Yu, 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 (68XX) 
1  Mathematical logic and foundations (03XX) 