HARP: A tableau-based theorem prover. This paper presents HARP, a complete, tableau-based theorem prover for first order logic, which is intended to be used both interactively and as an inference engine for Artificial Intelligence applications. Accordingly, HARP’s construction is influenced by the design goals of ‘naturalness’, efficiency, usefulness in an Artificial Intelligence environment, and modifiability of the control structure by heuristics. To achieve these goals, HARP accepts the entire language of first order logic, i.e. avoids conversion to any kind of normal form, and combines a proof condensation procedure with explicitly represented, declaratively formulated heuristics to construct and communicate its proofs in a format congenial to people. The proof condensation procedure makes proof shorter and more readable by excising redundancies from proof trees. Domain-independent heuristics are formulated to capture efficient and human-like deduction strategies and to rapidly detect certain types of nontheorems. Domain-dependent heuristics can be used to implement specific control regimes, e.g. to efficiently support inheritance. HARP’s architecture-and the concomitant ready extensibility of its control structure by declarative heuristic rules-renders it easy to let extralogical information, e.g. semantic and world knowledge, guide the search for proofs and help eliminate irrelevant premisses.

References in zbMATH (referenced in 16 articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
  2. Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
  3. Tsarkov, Dmitry; Horrocks, Ian; Patel-Schneider, Peter F.: Optimizing terminological reasoning for expressive description logics (2007)
  4. Hunter, Anthony: Logical comparison of inconsistent perspectives using scoring functions (2004) ioport
  5. Beckert, Bernhard: Depth-first proof search without backtracking for free-variable clausal tableaux (2003)
  6. Koshimura, Miyuki; Fujita, Hiroshi; Hasegawa, Ryuzo: Model generation with Boolean constraints (2001)
  7. Donini, F. M.; Massacci, F.: EXPtime tableaux for ALC (2000)
  8. Hähnle, Reiner; Pape, Christian: Ordered tableaux: extensions and applications (1997)
  9. Iwanuma, Koji: Lemma matching for a PTTP-based top-down theorem prover (1997)
  10. Baumgartner, Peter; Furbach, Ulrich; Niemelä, Ilkka: Hyper tableaux (1996)
  11. Beckert, Bernhard; Hähnle, Reiner; Oel, Peter; Sulzmann, Martin: The tableau-based theorem prover (_3\mkern-4mu T^\mkern-5mu A\mkern-5mu P) Version 4.0 (1996)
  12. Beckert, Bernhard; Posegga, Joachim: lean(T^ AP): Lean tableau-based deduction (1995)
  13. Klingenbeck, Stefan; Hähnle, Reiner: Semantic tableaux with ordering restrictions (1994)
  14. Lorenz, Sven: A tableau prover for domain minimization (1994)
  15. Murray, Neil V.; Rosenthal, Erik: On the relative merits of path dissolution and the method of analytic tableaux (1994)
  16. Schumann, J.: Tableau-based theorem provers: Systems and implementations (1994) ioport