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.

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.

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).