Title: On the relation between resolution based and completion based theorem proving
Abstract: Completion theorem proving, as proposed by J. Hsiang (1982), is based on the observation that proving a first order formula is equivalent to solving an equational system over a boolean polynomial ring. The latter can be accomplished, by completing the set of rewrite rules obtained from the equational system. This method's basic deduction rule is the generation of a new rule from a divergent critical pair obtained by superposition of two rules. This paper relates superposition to the resolution rule, which is the basis of resolution theorem proving, extending Dietrich's result on the correspondence between completion and resolution from Horn clauses to arbitrary clauses. It is shown that each completion deduction that follows Hsiang's N-strategy can be partitioned into sequences of superpositions that correspond to hyperresolution steps. However, such a correspondence does not exist for arbitrary completion deductions: There is a class of clause sets that preclude resolution refutations using each clause only once — a result which was given by R. Shostak — but admit completion refutations with this property, that is, such a completion refutation is shorter than any resolution refutation can be. Furthermore, we show by means of Shostak's theorem that the language of rings and ideals is well suited for short and elegant proofs of theorems about resolution deductions.
Publication Year: 1991
Publication Date: 1991-01-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 1
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot