-
-
Peter Baumgartner.
Logical Engineering with Instance-Based Methods.
In Frank Pfenning, editor, CADE-21 -- The 21st International
Conference on Automated Deduction, volume 4603 of Lecture Notes in
Artificial Intelligence, pages 404--409. Springer, July 2007.
[ bib |
.pdf ]
-
-
Frank Pfenning, editor.
Automated Deduction -- CADE-21, volume 4603 of Lecture
Notes in Artificial Intelligence. Springer, 2007.
[ bib ]
-
-
Peter Baumgartner, Ulrich Furbach, and Björn Pelzer.
Hyper Tableaux with Equality.
In Frank Pfenning, editor, CADE-21 -- The 21st International
Conference on Automated Deduction, volume 4603 of Lecture Notes in
Artificial Intelligence, pages 492--507. Springer, 2007.
[ bib |
.pdf ]
In most theorem proving applications, a proper treatment of
equational theories or equality is mandatory. In this paper we show
how to integrate a modern treatment of equality in the hyper tableau
calculus. It is based on splitting of positive clauses and an adapted
version of the superposition inference rule, where equations used for
paramodulation are drawn (only) from a set of positive unit clauses,
the candidate model. The
calculus also features a generic, semantically justified
simplification rule which covers many redundancy elimination techniques
known from superposition-style theorem proving.
Our main theoretical result is the soundness and completeness of the
calculus. The calculus is implemented, and we also report on
practical experiments.