Refinements of theory model elimination and a variant without contrapositives
Peter Baumgartner · 1994
. Theory Reasoning means to build-in certain knowledge about a problem domain into a deduction system or calculus, such as model elimination. We present several complete versions of highly restricted theory model elimination (TME) calculi. These restrictions allow (1) to keep fewer path literals in extension steps than in related calculi, and (2) to discard proof attempts with multiple occurrences of literals along a path (i.e. regularity holds). On the other hand, we obtain by small modifications to TME versions which do not need contrapositives (a la Near-Horn Prolog). We show how regularity can be adapted for these versions. The independence of the goal computation rule holds for all variants. Comparative runtime results for our PTTP-implementations are supplied. 1 Introduction and Preliminaries The model elimination calculus is a goal-oriented, linear and refutationally complete calculus for first order clause logic [15]. It is the base of numerous proof procedures for first order...