Peter Baumgartner.
An Ordered Theory Resolution Calculus.
In A. Voronkov, editor, Logic Programming and Automated Reasoning (Proceedings), volume 624 of Lecture Notes in Artificial Intelligence, pages 119-130, St. Petersburg, Russia, July 1992. Springer. [ bib | .pdf ]
In this paper we present an ordered theory resolution calculus and prove its completeness. Theory reasoning means to relieve a calculus from explicitly drawing inferences in a given theory by special purpose inference rules (e.g. E-resolution for equality reasoning). We take advantage of orderings (e.g. simplification orderings) by disallowing to resolve upon clauses which violate certain maximality constraints; stated positively, a resolvent may only be built if all the selected literals are maximal in their clauses. By this technique the search space is drastically pruned. As an instantiation for theory reasoning we show that equality can be built in by rigid E-unification.

 
Peter Baumgartner.
A Model Elimination Calculus with Built-in Theories.
In H.-J. Ohlbach, editor, GWAI-92 - Proceedings of the 16th German Workshop on Artificial Intelligence, volume 671 of Lecture Notes in Artificial Intelligence, pages 30-42. Springer, 1992. [ bib | .pdf ]
The model elimination calculus is a linear, refutationally complete calculus for first order clause logic. We show how to extend this calculus with a framework for theory reasoning. Theory reasoning means to separate the knowledge of a given domain or theory and treat it by special purpose inference rules. We present two versions of theory model elimination: the one is called total theory model elimination (which allows e.g. to treat equality in a rigid E-resolution style), and the other is called partial theory model elimination (which allows e.g. to treat equality in a paramodulation style).

 
Peter Baumgartner.
A Model Elimination Calculus with Built-In Theories.
In Fronhöfer, Hähnle, Käufl, editor, Theorem Proving with Analytic Tableaux and Related Methods, number 8/92 in Technical Report, 1992. [ bib ]
 
Peter Baumgartner.
Partial Unification for Ordered Theory Resolution.
In F. Baader, J. Siekmann, and W. Snyder, editors, 6th International Workshop on Unification. IBFI Dagstuhl, 1992.
Dagstuhl Seminar Report 42. [ bib ]
 
Peter Baumgartner.
Consolution as a Framework for Comparing Calculi.
In Fronhöfer, Hähnle, Käufl, editor, Theorem Proving with Analytic Tableaux and Related Methods, number 8/92 in Technical Report, 1992. [ bib ]
 
Peter Baumgartner, Ulrich Furbach, and Uwe Petermann.
A Unified Approach to Theory Reasoning.
Fachberichte Informatik 15/92, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1992. [ bib | .pdf ]
Theory reasoning is a kind of two-level reasoning in automated theorem proving, where the knowledge of a given domain or theory is separated and treated by special purpose inference rules. We define a classification for the various approaches for theory reasoning which is based on the syntactic concepts of literal level - term level - variable level. The main part is a review of theory extensions of common calculi (resolution, model elimination and a connection method). In order to see the relationships among these calculi, we define a super-calculus called theory consolution. Completeness of the various theory calculi is proven. Finally, due to its relevance in automated reasoning, we describe current ways of equality handling.