Using Herby

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

Chapter 8 in Automated Theorem Proving, 2001, pp 97-112 from Springer

Abstract: Abstract This chapter describes how to use HERBY to prove theorems. The input to HERBY is a text file formatted in either its own HERBY/THEO format or in the format of the TPTP Problem Library. This is described in Section 8.1. HERBY saves the results in an output file, as described in Section 8.2. Options that the user can control are described in Section 8.3. User interaction during the search is described in Section 8.4. Examples of user options are presented in Section 8.5. Examples of HERBY’s output are given in Sections 8.6 and 8.7. The construction of a closed semantic tree is illustrated in Section 8.6. After finding a closed semantic tree, HERBY can construct a resolution-refutation proof using Algorithm 6.1, as illustrated in Section 8.7.

Keywords: Input File; Unit Clause; Semantic Tree; Generate Clause; User Option (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_8

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

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

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