Topics in Completion Theorem Proving

Abstract

Completion Theorem Proving is based on the observation that proving a formula is equivalent to solving a system of equations over a boolean polynomial ring. The latter can be accomplished by means of the completion of a set of rewrite rules Obtained from the equational system. This report deals with three problems concerning Completion Theorem Provers (CTPs): - Are multiple overlaps necessary for the completeness of CTPs? - How can simplification be interpreted in terms of resolution inference rules ? - How can polynomials efficiently be represented? The answer to the first question is “no”. Even more it is shown in this report that the removal of multiple overlap steps does not increase the length of completion refutations. This amounts to an extension of Dietrich’s (1986) result concerning the correspondence of completion proofs without simplification for Horn Logic to resolution proofs. Concerning the second question we show that simplification in general cannot be translated into resolution reduction rules. However, two special cases of reduction can be interpreted as subsumption deletion and replacement resolution, respectively. Changing the point of view, we can also identify resolution reduction rules, such as tautology elimination, merging and subsumption deletion, as part of CTPs without being explicitly defined as inference rules. The last section deals with the technical question of choosing a datastructure well suited for an efficient implementation of CTPs.