A Brief Introduction to Compile, Herby, and Theo

Monty Newborn ()
Additional contact information
Monty Newborn: McGill University, School of Computer Science

Chapter 1 in Automated Theorem Proving, 2001, pp 1-6 from Springer

Abstract: Abstract This book is about how computers prove theorems. In particular, it is about how two programs, HERBY and THEO, carry out this fascinating process. This first chapter briefly introduces the reader to these two programs and to a third called COMPILE. COMPILE prepares a theorem, transforming it into the required format, for HERBY and THEO. Once in the required format, HERBY and THEO can then attempt to find a proof. HERBY is a semantic-tree theorem-proving program. THEO is a resolution-refutation theorem-proving program. These three programs are written in ANSI C and compile using standard C compilers. They run under UNIX (and Linux, Solaris, FreeBSD, and AIX). IBM’s C compiler for AIX, Version 4.4, is included on the CD-ROM accompanying this text.

Date: 2001
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4613-0089-2_1

Ordering information: This item can be ordered from
http://www.springer.com/9781461300892

DOI: 10.1007/978-1-4613-0089-2_1

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().