Refinements and extensions of model elimination

Abstract

In this paper we present new refinements and extensions of the model elimination calculus. These refinements offer a smaller branching rate of the search space, but at the price that short proofs may no longer exist—a fact which becomes crucial for proof procedures which enumerate proofs by using an iterative deepening approach. In order to obtain shorter proofs the model elimination calculus can be extended by a further inference rule which facilitates the multiple use of the same subproofs. The new calculus is shown to have some very interesting properties, like the reversibility of subproofs and the possibility of cut elimination without affecting the proof length. These results enable us to state that the extended calculus, semantic trees, and linear resolution can mutually p-simulate each other.