SEMANTIC PARAMODULATION FOR HORN SETS (LOGIC, EQUALITY, THEOREM-PROVING)

A semantic restriction is presented for use with paramodulation (an inference rule for generalized equality substitution) in automated theorem-proving programs. The method applies to first-order formulas with equality whose clause forms are Horn sets. With the method, an interpretation is given to the program along with the set of clauses to be refuted. The intention is that the interpretation will serve as an example to guide the search for a refutation. The proof of the completeness of the method rests on new techniques involving the rearrangement of ground deductions. The semantic restriction was incorporated into an existing automated theorem-proving program, and a number of experiments were conducted on theorems in abstract algebra. Semantic paramodulation is an extension of set-of-support paramodulation, so a comparison of the two strategies was used as the basis for experimentation. The semantic searches performed markedly better than the corresponding set-of-support searches in many of the comparisons. The semantic restriction also makes the program less sensitive to the choice of rewrite rules and supported clauses.