hide
Free keywords:
-
Abstract:
Transformation--based systems for general E-unification
were first investigated by Gallier and Snyder. Their system extends
the well--known rules for syntactic unification by Lazy
Paramodulation, thus coping with the equational theory.
More recently, Dougherty and Johann improved on this method by
giving a restriction of the Lazy Paramodulation inferences. In this
paper, we show that their system can be further improved by a
stronger restriction on the applicability of Lazy
Paramodulation. It turns out that the framework of proof
transformations provides an elegant and natural means for proving
completeness of the inference system.
