A new hyperparamodulation for the equality relation (hl-resolution, k-pd link)
Young-Hwan Lim · 1985
Equality is an important relation and many theorems can be easily symbolized through its use. But it presents special strategic problems, both theoretical and practical, for theorem proving programs. A proposed inference rule called HL-resolution is intended to have the benefits of hyper steps while controlling the application of paramodulation. It generates a resolvent by building a paramodulation/demodulation link between two terms using a preprocessed plan as a guide. The rule is complete for E-unsatisfiable Horn sets. The completeness of the method has been proved by constructing a transforming process from an unrestricted paramodulation and resolution refutation into a corresponding HL-refutation. The linking process makes use of an equality graph which is constructed once at the beginning of the run. Once a pair of candidate terms 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. Furthermore, using the properties of links, pairs of end terms for inner level linking can be found easily. The method has been implemented on an existing theorem-proving system. A number of experiments were conducted on problems in abstract algebra and a comparison with set-of-support paramodulation was made.