Skip to main content
SpringerLink
Log in

Unification properties of commutative theories: A categorical treatment

  • Conference paper
  • First Online:
Category Theory and Computer Science

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

Abstract

A general framework for unification in “commutative” theories is investigated, which is based on a categorical reformulation of theory unification. This yields algebraic characterizations of unification type unitary (resp. finitary for unification with constants). We thus obtain the well-known results for abelian groups, abelian monoids and idempotent abelian monoids as well as some new results as corollaries to a general theorem. In addition, it is shown that constant-free unification problems in “commutative” theories are either unitary or of unification type zero and we give an example of a “commutative” theory of type zero.

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

  • Baader, F. (1987). Unification in Varieties of Idempotent Semigroups. Semigroup Forum 36.

    Google Scholar 

  • Baader, F. (1988). Unification in Commutative Theories. To appear in J. Symbolic Computation.

    Google Scholar 

  • Baader, F. (1989a). Characterizations of Unification Type Zero. Proceedings of the RTA '89 Chapel Hill (USA). Springer Lec. Notes Comp. Sci. 355.

    Google Scholar 

  • Baader, F. (1989b). Unification in Commutative Theories, Hilbert's Basis Theorem and Gröbner Bases. Preprint.

    Google Scholar 

  • Baader, F., Büttner, W. (1988). Unification in Commutative Idempotent Monoids. TCS 56.

    Google Scholar 

  • Buchberger, B. (1985). Gröbner Bases: An Algorithmic Method in Polynomial Ideal Theory. In Bose, N. K. (Ed.). Recent Trends in Multidimensional System Theory.

    Google Scholar 

  • Büttner, W. (1986). Unification in the Data Structure Multiset. J. Automated Reasoning 2.

    Google Scholar 

  • Clausen, M., Fortenbacher, A. (1988). Efficient Solution of Linear Diophantine Equations. To appear in J. Symbolic Computation, Special Issue on Unification.

    Google Scholar 

  • Clifford, A.H., Preston, G.B. (1967). The Algebraic Theory of Semigroups, Vol. 2. AMS Mathematical Surveys 7.

    Google Scholar 

  • Cohn, P.M. (1965). Universal Algebra. New York: Harper and Row.

    Google Scholar 

  • Fages, F. (1984). Associative-Commutative Unification. Proceedings of the CADE '84 Napa (USA). Springer Lec. Notes Comp. Sci. 170.

    Google Scholar 

  • Fages, F., Huet, G. (1986). Complete Sets of Unifiers and Matchers in Equational Theories. TCS 43.

    Google Scholar 

  • Fortenbacher, A. (1985). An Algebraic Approach to Unification under Associativity and Commutativity. Proceedings of the RTA '85 Dijon (France). Springer Lec. Notes Comp. Sci. 202.

    Google Scholar 

  • Freyd, P. (1964). Abelian Categories. New York: Harper and Row.

    Google Scholar 

  • Grätzer, G. (1968). Universal Algebra. Princeton: Van Nostrand Company.

    Google Scholar 

  • Herold, A. (1987). Combination of Unification Algorithms in Equational Theories. Ph.D. Dissertation, Universität Kaiserslautern.

    Google Scholar 

  • Herrlich, H., Strecker, G.E. (1973). Category Theory. Boston: Allyn and Bacon Inc.

    Google Scholar 

  • Huet, G. (1978). An Algorithm to Generate the Basis of Solutions to Homogeneous Diophantine Equations. Information Processing Letters 7.

    Google Scholar 

  • Huet, G. (1980). Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. ACM 27.

    Google Scholar 

  • Jacobson, N. (1980). Basic Algebra II. San Francisco: Freeman and Company.

    Google Scholar 

  • Jaffar, J., Lassez, J.L., Maher, M.J. (1984). A Theory of Complete Logic Programs with Equality. J. Logic Programming 1.

    Google Scholar 

  • Jouannaud, J.P. (1983). Confluent and Coherent Equational Term Rewriting Systems, Applications to Proofs in Abstract Data Types. Proceedings of the CAAP '83 Pisa (Italy). Springer Lec. Notes Comp. Sci. 159.

    Google Scholar 

  • Jouannaud, J.P., Kirchner, H. (1986). Completion of a Set of Rules Modulo a Set of Equations. SIAM J. Comp. 15.

    Google Scholar 

  • Kuich, W., Salomaa, A. (1986). Semirings, Automata, Languages. Berlin: Springer Verlag.

    Google Scholar 

  • Knuth, D.E. (1973). The Art of Computer Programming, Vol 2. Reading: Addison-Wesley.

    Google Scholar 

  • Kurosh, A.G. (1960). The Theory of Groups, Vol 1. New York: Chelsea Publishing Company.

    Google Scholar 

  • Lambert, J-L. (1987). Une borne pour les générateurs des solutions entières positives d' une équation diophantienne linéaire. CRASP 305.

    Google Scholar 

  • Lankford, D., Butler, G., Brady, B. (1984). Abelian Group Unification Algorithms for Elementary Terms. Contemporary Mathematics 29.

    Google Scholar 

  • Lawvere, F.W. (1963). Functional Semantics of Algebraic Theories. Ph.D. Dissertation, Columbia University.

    Google Scholar 

  • Livesey, M., Siekmann, J. (1978). Unification in Sets and Multisets. SEKI Technical Report, Universität Kaiserslautern.

    Google Scholar 

  • Makanin, G.S. (1977). The Problem of Solvability of Equations in a Free Semigroup. Mat. Sbornik 103. English transl. in Math USSR Sbornik 32 (1977).

    Google Scholar 

  • Mora, F. (1986). Gröbner Bases for Non-Commutative Polynomial Rings. Proceedings of the AAECC3. Springer Lec. Notes Comp. Sci. 228.

    Google Scholar 

  • Nash-Williams, C.St.J.A. (1963). On Well-Quasi-Ordering Finite Trees. Proc. Cambridge Philos. Soc. 59.

    Google Scholar 

  • Nevins, A.J. (1974). A Human Oriented Logic for Automated Theorem Proving. J. ACM 21.

    Google Scholar 

  • Niven, I., Zuckerman, H.S. (1972). An Introduction to the Theory of Numbers. New York: John Wiley and Sons.

    Google Scholar 

  • Nutt, W. (1988). Talk at the Second Workshop on Unification, Val d' Ajol (France).

    Google Scholar 

  • Peterson, G., Stickel, M. (1981). Complete Sets of Reductions for Some Equational Theories. J.ACM 28.

    Google Scholar 

  • Plotkin, G. (1972). Building-in Equational Theories. Machine Intelligence 7.

    Google Scholar 

  • Rydeheard, D.E., Burstall, R.M. (1985). A Categorical Unification Algorithm. Proceedings of the Workshop on Category Theory and Computer Programming. Springer Lec. Notes Comp. Sci. 240.

    Google Scholar 

  • Siekmann, J. (1986). Universal Unification. Proceedings of the 7th ECAI.

    Google Scholar 

  • Slage, J.R. (1974). Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity. J. ACM 21.

    Google Scholar 

  • Stickel, M. (1981). A Unification Algorithm for Associative-Commutative Functions. J. ACM 28.

    Google Scholar 

  • Stickel, M. (1985). Automated Deduction by Theory Resolution. J. Automated Reasoning 1.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Mathematische Maschinen und Datenverarbeitung (Informatik) 1, Universität Erlangen-Nürnberg, Martensstraße 3, 8520, Erlangen, F.R.G.

    Franz Baader

Authors
  1. Franz Baader
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

David H. Pitt David E. Rydeheard Peter Dybjer Andrew M. Pitts Axel Poigné

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baader, F. (1989). Unification properties of commutative theories: A categorical treatment. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds) Category Theory and Computer Science. Lecture Notes in Computer Science, vol 389. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018357

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51662-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation