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.
This work was funded by the German Ministry for Research and Technology (BMFT) under grant ITS 9103.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Dougherty, DJ. and Johann, P. An Improved General E-Unification Method. J. Symbolic Computation 14 (1992), 303–320.
Gallier, J. and Snyder, W. Complete Sets of Transformations for General E-unification. Theoretical Computer Science 67, 2 & 3 (1989), 203–260.
Snyder, W. A Proof Theory for General E-Unification. Birkhäuser, Boston 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Socher-Ambrosius, R. (1994). A refined version of general E-unification. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_48
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive