Skip to main content
SpringerLink
Log in

Unification in the union of disjoint equational theories: Combining decision procedures

  • Conference paper
  • First Online:
Automated Deduction—CADE-11 (CADE 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 607))

Included in the following conference series:

Abstract

Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms which compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms which just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures which works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories. As a consequence of this new method, we can for example show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol.

Our method can also be used to combine algorithms which compute finite complete sets of unifiers. Manfred Schmidt-Schauß' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also get the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.

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

  1. F. Baader, K.U. Schulz, “Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures,” DFKI Research Report RR-91–33.

    Google Scholar 

  2. L. Bachmair, Proof Methods for Equational Theories, Ph.D. Thesis, Dept. of Comp. Sci., University of Illinois at Urbana-Champaign, 1987.

    Google Scholar 

  3. A. Boudet, “Unification in a Combination of Equational Theories: An Efficient Algorithm,” Proceedings of the 10th International Conference on Automated Deduction, LNCS 449, 1990.

    Google Scholar 

  4. A. Boudet, J.P. Jouannaud, M. Schmidt-Schauß, “Unification in Boolean Rings and Abelian Groups,” J. Symbolic Computation 8, 1989.

    Google Scholar 

  5. H.-J. Bürckert, “Some Relationships Between Unification, Restricted Unification, and Matching,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.

    Google Scholar 

  6. H.-J. Bürckert, “A Resolution Principle for Clauses with Constraints,” Proceedings of the 10th International Conference on Automated Deduction, LNCS 449, 1990.

    Google Scholar 

  7. N. Dershowitz, J.P. Jouannaud, “Rewrite Systems,” In J. van Leeuwen (editor), Volume B of Handbook of Theoretical Computer Science, NorthHolland, 1990.

    Google Scholar 

  8. F. Fages, “Associative-Commutative Unification,” Proceedings of the 7th International Conference on Automated Deduction, LNCS 170, 1984.

    Google Scholar 

  9. A. Herold, “Combination of Unification Algorithms,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.

    Google Scholar 

  10. A. Herold, J.H. Siekmann, “Unification in Abelian Semigroups,” J. Automated Reasoning 3, 1987.

    Google Scholar 

  11. J.M. Howie, An Introduction to Semigroup Theory, London: Academic Press, 1976.

    Google Scholar 

  12. J. Jaffar, J.L. Lassez, M. Maher, “A Theory of Complete Logic Programs with Equality,” J. Logic Programming 1, 1984.

    Google Scholar 

  13. J. Jaffar, J.L. Lassez, “Constraint Logic Programming,” Proceedings of 14th POPL Conference, Munich, 1987

    Google Scholar 

  14. J.P. Jouannaud, H. Kirchner, “Completion of a Set of Rules Modulo a Set of Equations,” SIAM J. Computing 15, 1986.

    Google Scholar 

  15. J.P. Jouannaud, C. Kirchner, “Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification,” In J.-L. Lassez, G. Plotkin (editors), Alan Robinson's Anniversary Book, 1991.

    Google Scholar 

  16. D. Kapur, P. Narendran, “Complexity of Unification Problems with Associative-Commutative Operators,” Preprint, 1991. To appear in J. Automated Reasoning.

    Google Scholar 

  17. C. Kirchner, Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories equationnelles, Thèse d'Etat, Univ. Nancy, France, 1985.

    Google Scholar 

  18. C. Kirchner, H. Kirchner, “Constrained Equational Reasoning,” Proceedings of SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ACM Press, 1989.

    Google Scholar 

  19. M. Livesey, J.H. Siekmann, “Unification of AC-Terms (bags) and ACITerms (sets),” Internal Report, University of Essex, 1975, and Technical Report 3-76, Universität Karlsruhe, 1976.

    Google Scholar 

  20. G.S. Makanin, “The Problem of Solvability of Equations in a Free Semigroup,” Mat. USSR Sbornik 32, 1977.

    Google Scholar 

  21. G. Plotkin, “Building in Equational Theories,” Machine Intelligence 7, 1972.

    Google Scholar 

  22. M. Schmidt-Schauß, “Combination of Unification Algorithms,” J. Symbolic Computation 8, 1989.

    Google Scholar 

  23. K.U. Schulz, “Makanin's Algorithm — Two Improvements and a Generalization,” CIS-Report 91-39, CIS, University of Munich, 1991.

    Google Scholar 

  24. J.H. Siekmann, “Unification Theory: A Survey,” in C. Kirchner (ed.), Special Issue on Unification, Journal of Symbolic Computation 7, 1989.

    Google Scholar 

  25. M. Stickel, “A Complete Unification Algorithm for Associative-Commutative Functions,” Proceedings of the International Joint Conference on Artificial Intelligence, 1975.

    Google Scholar 

  26. M.E. Stickel, “A Unification Algorithm for Associative-Commutative Functions,” J. ACM 28, 1981.

    Google Scholar 

  27. M.E. Stickel, “Automated Deduction by Theory Resolution,” J. Automated Reasoning 1, 1985.

    Google Scholar 

  28. E. Tiden, “Unification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.

    Google Scholar 

  29. K. Yelick, “Unification in Combinations of Collapse Free Regular Theories,” J. Symbolic Computation 3, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DFKI, Stuhlsatzenhausweg 3, 6600, Saarbrücken 11, Germany

    Franz Baader

  2. CIS University Munich, Leopoldstr. 139, 8000, München 40, Germany

    Klaus U. Schulz

Authors
  1. Franz Baader
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus U. Schulz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baader, F., Schulz, K.U. (1992). Unification in the union of disjoint equational theories: Combining decision procedures. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_155

Download citation

  • DOI: https://doi.org/10.1007/3-540-55602-8_155

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-47252-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation