Well-behaved inference rules for first-order theorem proving (Q1272612)

Boolean ring based deduction was introduced independently by Jieh Hsiang in 1982, and by Deepak Kapur and Paliath Narendran in 1985. The Boolean ring has ``exclusive OR'' as addition operator, and ``AND'' as multiplication operator, and its main advantage is a canonical rewrite system, so that every expression has unique normal form. In Boolean ring based theorem proving, the quantifier-free formulas representing the problem are transformed into equations in the Boolean ring (e.g. \(m_1+m_2+ \cdots m_k =0\), where the \(m_i\) are products of atoms), and fed into an inference engine with overlap inference rules (that generate new equations from the existing ones), and simplification inference rules (that reduce equations). Hsiang's approach emphasized refutational theorem proving, and strategies that are complete while doing as few overlaps as possible. The \(N\)-strategy was a clausal strategy allowing only overlaps where at least one premise is an \(N\)-rule (i.e., \(m_1=0)\), and only \(N\)-rules and \(P\)-rules (i.e., \(A=1\) with \(A\) an atom) as simplifiers, so that matching on atoms or monomials sufficed. The approach of Kapur-Narendran emphasized saturation (as in Buchberger's algorithm to generate Gröbner bases), and therefore required to orient all equations into rewrite rules, consider all overlaps, and all simplifications, involving matching over polynomials and repeated applications of distributivity. The saturation philosophy was continued by Leo Bachmair and Nachum Dershowitz (``Inference rules for rewrite-based first-order theorem proving'', LICS-87) with a Boolean ring method inspired by Knuth-Bendix completion (that generates a confluent rewrite system for a set of equations). This method improved its predecessor by handling equations, requiring fewer overlaps, and adopting a less expensive form of rewriting (by oriented instances of equations, e.g., \(m_1\sigma \succ (m_2+ \dots m_k) \sigma\), so that matching on monomials sufficed, but with repeated application of distributivity). The refutational philosophy was continued by Jürgen Müller and Rolf Socher-Ambrosius in 1987-88 with a new \(N\)-strategy, considering single parallel overlaps instead of multiple sequential overlaps: single parallel overlap unifies atoms instead of monomials, and handles all occurrences of an atom in a polynomial in one step by factoring them out. The \(N\)-strategy required to transform first quantifier-free formulas into clauses, because if quantifier-free formulas are turned directly into equations there may be no \(N\)-rules even if the set is unsatisfiable. In 1994, Hantao Zhang proposed the Odd-strategy, that uses odd rules (i.e., \(m_1+\dots m_k=0\) where \(k\) is odd) instead of \(N\)-rules, eliminating the intermediate clausal form, and overlaps on maximal atoms only in the odd rule. The present paper presents two superposition inference rules that generalize odd-superposition and prove them complete with the set-of-support, linear, semantic and lock strategies. The generalization, which drops the conditions of the odd premise and maximal atom, may not be good in practice, because it may imply a larger search space. However, the results of completeness with semantic strategy and lock strategy restore the conditions (the odd strategy is a special case of semantic strategy assuming an interpretation that makes all atoms true); although locking uses an arbitrary ordering (the odd strategy used a complete simplification ordering), and the usage of ``semantic strategy'' in this paper does not seem correct, because a semantic strategy not only requires that at least one premise is false in the interpretation \(I\), but also that only formulas false in \(I\) are generated (thus the odd-strategy is not a semantic strategy either). Completeness with simplification by \(N\)-rules, \(P\)-rules and as in the odd-strategy is stated but not proved in this paper. The proof of completeness is obtained by defining sufficient conditions and showing that the inference rules satisfy them, which may represent a general framework for such proofs.