A New Hyperparamodulation Strategy for the Equality Relation

Abstract

Equality is an i.mportant relation and ~aa.ny theoreas can be easily symbolized through it's use. A proposed inference rule called HL-resolution is intended to have the benefits of hyper steps while controlling the application of paraiiOdulation. It generates a resolvent by building a paraiiOdulation and demodulation link between two teras using a preprocessed plan as a guide. The rule is complete for E-unsatisfiable Horn sets. The linking process makes use of an equality graph which is constructed once at the beginnlog of the run. Once a pair of candidate teras for HL-resolution is chosen in the search, potential linkages can be found and tested for compatibility efficiently by looking at the paths in the graph. The method was t.pla.ented on an existing theorem-proving systea. A number of experiments were conducted on probleas in abstract algebra and a comparison with set-of-support paramodulation was made.