Using Theo

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

Chapter 10 in Automated Theorem Proving, 2001, pp 139-159 from Springer

Abstract: Abstract This chapter describes how to use THEO to prove theorems. The input to THEO is a text file formatted either in its own HERBY/THEO format or in the format of the TPTP Problem Library. This is described in Section 10.1. THEO saves the results in an output file, as described in Section 10.2. Options that the user can control are described in Section 10.3. User interaction during the search is described in Section 10.4. The printout produced by THEO when proving a theorem is presented in Section 10.5. The printout when using the d1 option is presented in Section 10.6. This option allows the user to follow THEO’s progress in constructing a proof. Proving a set of theorems without user intervention is described in Section 10.7.

Keywords: Search Tree; Output File; Unit Clause; Hash Code; Simplification Phase (search for similar items in EconPapers)
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_10

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

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

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 ().