: Ulrich Furbach, Margret Gross-Hardt, Thomas Kleemann, and Peter Baumgartner.
Optimizing the Evaluation of XPath Using Description Logics.
In Dietmar Seipel, Michael Hanus, Ulrich Geske, and Oskar Bartenstein, editors, Applications of Declarative Programming and Knowledge Management (INAP/WLP 2004), volume 3392 of Lecture Notes in Artificial Intelligence. Springer Verlag, Berlin, Heidelberg, New-York, March 2005. [ bib ]
: Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, editors.
Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004), volume 125 of Electronic Notes in Theoretical Computer Science. Elsevier, 2005. [ bib | http ]
: Robert Nieuwenhuis, editor.
Automated Deduction -- CADE-20, volume 3632 of Lecture Notes in Artificial Intelligence. Springer, 2005. [ bib ]
: Peter Baumgartner, Ulrich Furbach, and Adnan H. Yahya.
Automated Reasoning, Knowledge Representation and Management.
KI, 1:5--11, 2005. [ bib ]
: Peter Baumgartner and Cesare Tinelli.
The Model Evolution Calculus with Equality.
In Nieuwenhuis [3], pages 392--408. [ bib | .pdf ]
In many 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 Model Evolution calculus (ME), a first-order version of the propositional DPLL procedure. The new calculus, MEE, is a proper extension of the ME calculus without equality. Like ME it maintains an explicit “candidate model”, which is searched for by DPLL-style splitting. For equational reasoning MEE uses an adapted version of the ordered paramodulation inference rule, where equations used for paramodulation are drawn (only) from the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main result is the correctness of the MEE calculus in the presence of very general redundancy elimination criteria.