

Ulrich Furbach, Margret GrossHardt, 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, NewYork,
March 2005.
[ bib ]


Peter Baumgartner and Cesare Tinelli.
The Model Evolution Calculus with Equality.
In Nieuwenhuis [4], pages 392408.
[ 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 firstorder 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 DPLLstyle 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 superpositionstyle theorem proving.
Our main result is the correctness of the MEE calculus in the
presence of very general redundancy elimination criteria.


Peter Baumgartner, Ulrich Furbach, and Adnan H. Yahya.
Automated Reasoning, Knowledge Representation and
Management.
KI, 1:511, 2005.
[ bib ]


Robert Nieuwenhuis, editor.
Automated Deduction  CADE20, volume 3632 of Lecture
Notes in Artificial Intelligence. Springer, 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 ]