Ordering-Based Strategies for Horn Clauses

Abstract

Two new theorem-proving procedures for equational Horn clauses are presented. The largest literal is selected for paramodulation in both strategies, except that one method treats positive literals as larger than negative ones and results in a unit strategy. Both use term orderings to restrict paramodulation to potentially maximal sides of equations and to increase the amount of allowable simplification (demodulation). Completeness is shown using proof orderings. 1 Introduction The completeness of positive-unit resolution for sets of Horn clauses p 1 \\Delta \\Delta \\Delta pn ) pn+1 is well-known. An advantage of a unit strategy is that the number of literals in clauses never grows; it suffers from the disadvantage of being a bottom-up method. Ordered resolution, in which the literals of each clause are arranged in a linear order ? and only the largest literal may serve as a resolvent, is also complete for Horn clauses [ Boyer, 1971 ] . The purpose here is to design Horn clause strate...