A disjunctive positive refinement of model elimination and its application to subsumption deletion (Q1369080)

Model elimination (ME) is one of the most successful inference systems for fully automated theorem proving. This paper is an interesting study of how to enhance ME, presented here in a tableaux-based formalism, with subsumption, which is a powerful mechanism for redundancy control in resolution-based theorem proving. This combination is problematic for several reasons. First, one needs to define a subsumption relation among tableaux. If the subsumption relation considers only the leaves -- or active nodes -- in the tableaux, the resulting calculus is incomplete (roughly speaking, this is because ME needs information about the ancestors). On the other hand, if the subsumption relation involves comparing the entire tableaux, it becomes an expensive operation. Second, the inference system of ME is usually coupled with a backward-reasoning search plan, such as depth-first search with iterative deepening. The resulting strategy stores only the most recently generated tableau, so that it does not have multiple tableaux whom it can apply subsumption to. The first problem is addressed by defining a refinement of ME -- called disjunctive positive ME or DPME -- where only positive ancestors coming from non-Horn clauses are relevant. This reduces the number of ancestors that subsumption needs to check. The second problem is addressed by coupling ME with a forward-reasoning search plan. Instead of enumerating tableaux by backtracking, the strategy generates all tableaux, and subsumption may apply. In this context, DPME with subsumption is shown to be complete. The paper also studies other refinements of ME and reports on a set of experiments with various theorem provers. In summary, this is very good reading for whoever is interested in combinations of forward and backward reasoning in theorem proving. A recent paper on the same subject is: \textit{M. P. Bonacina} and \textit{J. Hsiang}, ``On semantic resolution with lemmaizing and contraction and a formal treatment of caching'', New Gener. Comput. 16, No. 2 (1998).