MPI-I-93-237
A refined version of general E-unification
Socher-Ambrosius, Rolf
October 1993, 12 pages.
.
Status: available - back from printing
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.
-
MPI-I-93-237.pdf
- Attachement: MPI-I-93-237.ps (1558 KBytes); MPI-I-93-237.pdf (149 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-237
BibTeX
@TECHREPORT{Socher-Ambrosius93b,
AUTHOR = {Socher-Ambrosius, Rolf},
TITLE = {A refined version of general E-unification},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-93-237},
MONTH = {October},
YEAR = {1993},
ISSN = {0946-011X},
}