Skip to main content
SpringerLink
Log in

A new approach to universal unfication and its application to AC-unification

  • Conference paper
  • First Online:
9th International Conference on Automated Deduction (CADE 1988)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 310))

Included in the following conference series:

Abstract

A complete unification algorithm for simple theories is described. This algorithm is an extension of the variable abstraction approach. Since the associative-commutative (AC) theory is simple, an immediate consequence of this algorithm is a new AC-unification procedure. A partial correctness proof is given and some preliminary termination results for the AC case are presented.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Burris, S., Sankappanavar, H.P. (1981). A Course in Universal Algebra, Springer-Verlag.

    Google Scholar 

  • Bürckert, H.-J., Herold, A., and Schmidt-Schauß, M. (1987). On Equational Theories, Unification and Decidability, Proc. of RTA'87, Pierre Lescanne, ed., Springer-Verlag, LNCS 256, 204–215.

    Google Scholar 

  • Fages, F. and Huet, G. (1983). Unification and Matching in Equational Theories, Proc. of CAAP'83, Springer-Verlag, LNCS 159, 205–220.

    Google Scholar 

  • Fay, M. (1979). First Order Unification in an Equational Theory, Proc. of 4th Workshop on Automated Deduction, 161–167.

    Google Scholar 

  • Franzen, M. (1988). A Unification Algorithm for Simple Equational Theories, Doctoral Thesis, Northwestern University, forthcoming.

    Google Scholar 

  • Gallier, J.H. and Snyder, W. (1987). A Genereal Complete E-Unification Procedure, Proc. of RTA'87, Pierre Lescanne, ed., Springer-Verlag, LNCS 256, 216–227.

    Google Scholar 

  • Herold, A. (1982). Universal Unification and a Class of Equational Theories, Proc. of GWAI-82 (ed. W. Wahlster), Springer-Verlag, IFB-82, 177–190.

    Google Scholar 

  • Herold, A. (1985). A Combination of Unification Algorithms, in Proc. of 8th CADE, Springer-Verlag, LNCS 230, 450–469.

    Google Scholar 

  • Huet, G., Oppen, D.C. (1980). Equations and Rewrite Rules: A Survey, in Formal Languages: Perspectives and Open Problems, R. Book, ed., Academic Press, 349–405.

    Google Scholar 

  • Hullot, J.M. (1980). Canonical Forms and Unification, Proc. of 5th CADE, Springer-Verlag, LNCS 87, 318–334.

    Google Scholar 

  • Kirchner, C. (1985). Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories equationelles, Thèse de doctorat d'état, Université de Nancy I.

    Google Scholar 

  • Kirchner, C. (1986). Computing Unification Algorithms, 1st IEEE Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 1986, 206–216.

    Google Scholar 

  • Livesey, M., Siekmann, J. (1976). Unification of A + C Terms (Bags) and A + C + I Terms (Sets), Technical Report Interner Bericht Nr. 3/76, Institut für Informatik I, Universität Karlsruhe.

    Google Scholar 

  • Martelli, A., Moiso, C., Rossi, G.F. (1986). An Algorithm for Unification in Equational Theories, Proc. 1986 Symposium on Logic Programming, Salt Lake City, 180–186.

    Google Scholar 

  • Martelli, A., Montanari, U. (1982). An Efficient Unification Algorithm, ACM TOPLAS, Vol. 4, No. 2, 258–282.

    Article  Google Scholar 

  • Siekmann, J., Szabo, P. (1981). Universal Unification and Regular ACFM Theories, Proc. of IJCAI-81, Vancouver.

    Google Scholar 

  • Siekmann, J. (1984). Universal Unification, Proc. of 7th CADE, Springer-Verlag, LNCS 170, 1–42.

    Google Scholar 

  • Siekmann, J. (1986). Unification Theory, Proc. of ECAI'86, Vol. II, vi-xxxv.

    Google Scholar 

  • Stickel, M.E. (1981). A Unification Algorithm for Associative-Commutative Functions, JACM, vol. 28, 423–434.

    Article  Google Scholar 

  • Tiden, E. (1986). Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols, Proc. of 8th CADE, Springer-Verlag, LNCS 230, 431–449.

    Google Scholar 

  • Yelick, K. (1985). Combining Unification Algorithms for Confined Regular Equational Theories, Proc. of RTA'85, Springer-Verlag, LNCS 202, 365–380.

    Google Scholar 

  • Yelick, K. (1987). Unification in Combinations of Collapse-Free Regular Theories, J. Symbolic Computation, vol. 3, 153–181.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, Northwestern University, USA

    Mark Franzen

  2. Department of Computer Science, Northwestern University, USA

    Lawrence J. Henschen

Authors
  1. Mark Franzen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lawrence J. Henschen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ewing Lusk Ross Overbeek

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Franzen, M., Henschen, L.J. (1988). A new approach to universal unfication and its application to AC-unification. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012863

Download citation

  • DOI: https://doi.org/10.1007/BFb0012863

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19343-2

  • Online ISBN: 978-3-540-39216-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation