Abstract
We present restricted T-unification that is unification of terms under a given equational theory T with the restriction that not all variables are allowed to be substituted. Some relationships between restricted T-unification, unrestricted T-unification and T-matching (one-sided T-unification) are established. Our main result is that, in the case of an almost collapse free equational theory the most general restricted unifiers and for certain termpairs the most general matchers are also most general unrestricted unifiers, this does not hold for more general theories. Almost collapse free theories are theories, where only terms starting with projection symbols may collapse (i.e to be T-equal) to variables.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Burris S. & Sankappanavar H.P. [1983]: A Course in Universal Algebra; Springer, New York-Heidelberg-Berlin
Bürckert H.-J. [1986]: Some Relationships Between Unification, Restricted Unification, and Matching; SEKI-Report, Universität Kaiserslautern
Eisinger N. [1981]: Subsumption and Connection Graphs; Proc. IJCAI-81, Vancouver
Fages F. & Huet G. [1983]: Complete Sets of Unifiers and Matchers in Equational Theories; Proc. Caap-83, Springer Lec.Notes Comp.Sci. 159
Grätzer G. [1979]: Universal Algebra; Springer, New York-Heidelberg-Berlin
Herold A. [1983]: Some Basic Notions of First-Order Unification Theory, SEKI-Memo, Univ. Karlsruhe
Herold A. [1985]: A Combination of Unification Algorithms; SEKI-Memo, Univ. Kaiserslautern
Huet G. [1976]: Resolution d'Equations dans les Languages d'Ordre 1,2,...,ω, These d'Etat, Univ. Paris VIII
Huet G. & Oppen D.C. [1980]: Equations and Rewrite Rules (Survey); Technical Report, SRI International
Kowalski R. [1975]: A Proof Procedure Using Connection Graphs; J. ACM 22,4
Loveland D. [1978]: Automated Theorem Proving; North-Holland, Amsterdam-New York-Oxford
Plonka J. [1969]: On Equational Classes of Abstract Algebras Defined by Regular Equations; Fund. Math. LXIV
Raph K.M.G. [1984]: The Markgraf Karl Refutation Procedure (MKRP); SEKI-Memo, Univ. Kaiserslautern
Siekmann J. [1984]: Universal Unification (Survey); Proc. 7th CADE, Springer Lec Notes Comp. Sci. 170
Siekmann J. [1986]: Unification Theory; Proc. 7th ECAI, Brighton, to appear
Szabo P. [1982]: Unifikationstheorie Erster Ordnung (in german), Dissertation, Univ. Karlsruhe
Taylor W. [1979]: Equational Logic (Survey); Houston J. Math. 5
Tiden E. [1985]: Unification in Combination of Theories with Disjoint Sets of Function Symbols, Royal Inst. Techn., Dep. Comp. Sci., Stockholm
Yelick K. [1985]: Combining Unification Algorithms for Confined Regular Equational Theories; Proc. Rewriting Technics and Applications, Springer Lec Notes Comp. Sci. 202
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bürckert, HJ. (1986). Some relationships between unification, restricted unification, and matching. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_116
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_116
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive