Strict Basic Superposition

It is a well-known fact that some form of factoring is necessary for completeness of paramodulation-based calculi of general first-order clauses. In this paper we give an overview of some existing formalizations of factoring, their related paramodulation-based calculi, and corresponding completeness results. We also propose a factored superposition rule that "combines" usual superposition and factoring in a way similar to the rule presented in Moser et al. (1995). The advantage of our factored superposition rule is that it can be used in methods that combine bottom-up and top-down reasoning (like equality elimination for tableau method, see Degtyarev and Voronkov (2001)) without compromising completeness in presence of (the basic version of) tautology deletion and subsumption rules. 1 Ordered factoring We first consider the o-factoring rule, introduced in Hsiang and Rusinowitch (1986) as an inference rule of their ordered paramodulation calculus. If L1, . . . , Lk are litera...

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Leo Bachmair, Harald Ganzinger
• Keywords: CADE 1998, Factored Superposition Rule, Factoring Inference Rule, Inference Rule, Logical Reasoning