On Arbitrary Selection Strategies for Basic Superposition
Vladimir Aleksić, Anatoli Degtyarev · 2008
Abstract. For first-order Horn clauses without equality, resolution is complete with an arbitrary selection of a single literal in each clause [dN 96]. Here we extend this result to the case of clauses with equality for superposition-based inference systems. Our result is a generalization of the result given in [BG 01]. We answer their question about the com-pleteness of a superposition-based system for general clauses with an arbitrary selection strategy, provided there exists a refutation without applications of the factoring inference rule. 1