×

zbMATH — the first resource for mathematics

Combination problems for commutative/monoidal theories or how algebra can help in equational unification. (English) Zbl 0853.03008
Summary: We study the class of theories for which solving unification problems is equivalent to solving systems of linear equations over a semiring. It encompasses important examples like the theories of Abelian monoids, idempotent Abelian monoids, and Abelian groups. This class has been introduced by the authors independently of each other as “commutative theories” (Baader) and “monoidal theories” (Nutt).
We show that commutative theories and monoidal theories indeed define the same class (modulo a translation of the signature), and we prove that it is undecidable whether a given theory belongs to it. In the remainder of the paper we investigate combinations of commutative/monoidal theories with other theories. We show that finitary commutative/monoidal theories always satisfy the requirements for applying general methods developed for the combination of unification algorithms for disjoint equational theories.
Then we study the adjunction of monoids of homomorphisms to commutative/monoidal theories. This is a special case of a non-disjoint combination, which has an algebraic counterpart in the corresponding semiring. By studying equations over this semiring, we identify a large subclass of commutative/monoidal theories that are of unification type zero. We also show with methods from linear algebra that unitary and finitary commutative/monoidal theories do not change their unification type when they are augmented by a finite monoid of homomorphisms, and how algorithms for the extended theory can be obtained from algorithms for the basic theory.

MSC:
03C05 Equational classes, universal algebra in model theory
08A70 Applications of universal algebra in computer science
18E05 Preadditive, additive categories
16Y60 Semirings
68W30 Symbolic computation and algebraic computation
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baader, F.: Unification in Commutative Theories. J. Symb. Computation8, 479-497 (1989) · Zbl 0689.68039 · doi:10.1016/S0747-7171(89)80055-0
[2] Baader, F.: Unification Properties of Commutative Theories: A Categorical Treatment. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds.) Proceedings of the Conference on Category Theory and Computer Science. Lecture Notes in Computer Science, Vol. 389. Berlin, Heidelberg, New York: Springer 1989 · Zbl 0689.68039
[3] Baader, F.: Unification in Commutative Theories, Hubert’s Basis Theorem, and Gröbner Bases. J. ACM40, 477-503 (1993) · Zbl 0791.68146 · doi:10.1145/174130.174133
[4] Baader, F., Nutt, W.: Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification. In: Book, R. (ed.) Proceedings of the 4th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, Vol 488. Berlin, Heidelberg, New York: Springer 1991 · Zbl 0853.03008
[5] Baader, F., Schulz, K. U.: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. In: Kapur, D. (ed.) Proceedings of the 11th International Conference on Automated Deduction. Lecture Notes in Computer Science, Vol. 607. Berlin, Heidelberg, New York: Springer 1992 · Zbl 0925.03084
[6] Baader, F., Siekmann, J. H.: Unification Theory. In: Gabbay, D. M., Hogger, C. J., Robinson, J. A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford: Oxford University Press 1994
[7] Bachmair, L.: Canonical Equational Proofs. Boston, Basel, Berlin: Birkhäuser 1991 · Zbl 0732.68094
[8] Cohn, P. M.: Universal Algebra. New York: Harper and Row 1965 · Zbl 0141.01002
[9] Comon, H., Haberstrau, M., Jouannaud, J.-P.: Decidable Problems in Shallow Equational Theories. In: Scedrov, A. (ed.) Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science. Washington D.C.: IEEE Computer Society Press 1992
[10] Davis, M.: Unsolvable Problems. In: Barwise, J. (ed.) Handbook of Mathematical Logic. Amsterdam: Elsevier Science Publishers 1977
[11] Fay, M.: First-order Unification in an Equational Theory. In: Proceedings 4th Workshop on Automated Deduction 1979
[12] Fitting, M.: Basic Modal Logic. In: Gabbay, D. M., Hogger, C. J., Robinson, J. A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford: Oxford University Press 1993
[13] Gallier, J., Raatz, S.: SLD-Resolution Methods for Horn Clauses with Equality Based onE-Unification. In: Keller, R. M. (ed.) Proceedings of the 3rd IEEE Symposium on Logic Programming. Washington D.C.: IEEE Computer Society Press 1986 · Zbl 0668.68111
[14] Gallier, J., Snyder, S.: Complete Sets of Transformations for General E-Unification. Theor. Comput. Sci.27, 203-260 (1989) · Zbl 0686.68024 · doi:10.1016/0304-3975(89)90004-2
[15] Grätzer, G.: Universal Algebra. Princeton: Van Nostrand 1968
[16] Herrlich, H., Strecker, G. E.: Category Theory. Boston: Allyn and Bacon 1973 · Zbl 0265.18001
[17] Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. ACM27, 797-821 (1980) · Zbl 0458.68007 · doi:10.1145/322217.322230
[18] Jaffar, J., Lassez, J. L., Maher, M.: A Theory of Complete Logic Programs with Equality. J. Logic Programming1, 211-224 (1984) · Zbl 0584.68021 · doi:10.1016/0743-1066(84)90010-4
[19] Jouannaud, J. P., Kirchner, H.: Completion of a Set of Rules Modulo a Set of Equations. SIAM J. Comp.15, 1155-1194 (1986) · Zbl 0665.03005 · doi:10.1137/0215084
[20] Kirchner, C., Klay, F.: Syntactic Theories and Unification. In: Mitchell, J. (ed.) Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. Washington D.C.: IEEE Computer Society Press 1990
[21] Lawvere, F. W.: Functional Semantics of Algebraic Theories. Ph.D. Thesis, Columbia University, New York (1963) · Zbl 0119.25901
[22] Lemmon, E. J.: Algebraic Semantics for Modal Logics I. J. Symbolic Logic31, 46-65 (1966) · Zbl 0147.24805 · doi:10.2307/2270619
[23] Livesey, M., Siekmann, J.: Unification of Bags and Sets. SEKI-MEMO 76-II, Institut für Informatik I, Universität Karlsruhe (1976)
[24] Nevins, A. J.: A Human Oriented Logic for Automated Theorem Proving. J. ACM21, 606-621 (1974) · Zbl 0332.68061 · doi:10.1145/321850.321858
[25] Nutt, W.: Unification in Monoidal Theories, Presentation at the Second Workshop on Unification. Val d’Ajol, France, (1988)
[26] Nutt, W., Réty, P., Smolka, G.: Basic Narrowing Revisited. J. Symb. Computation7, 295-317 (1989) · Zbl 0682.68094 · doi:10.1016/S0747-7171(89)80014-8
[27] Nutt, W.: The Unification Hierarchy is Undecidable. J. Automated Reasoning7, 369-381 (1991) · Zbl 0744.03016 · doi:10.1007/BF00249020
[28] Nutt, W.: Unification in Monoidal Theories. In: Stickel, M. (ed.) Proceedings 10th International Conference on Automated Deduction. Lecture Notes in Computer Science, Vol. 499. Berlin, Heidelberg, New York: Springer 1990
[29] Nutt, W.: Unification in Monoidal Theories is Solving Linear Equations over Semirings. Technical Report RR-92-01, DFKI Saarbrücken (1992)
[30] Peterson, G., Stickel, M.: Complete Sets of Reductions for Some Equational Theories. J. ACM28, 233-264 (1981) · Zbl 0479.68092 · doi:10.1145/322248.322251
[31] Plotkin, G.: Building in Equational Theories. Machine Intelligence7, 73-90 (1972) · Zbl 0262.68036
[32] Rotman, J. J.: The Theory of Groups. Boston: Allyn and Bacon 1973 · Zbl 0262.20001
[33] Schmidt-Schauß, M.: Combination of Unification Algorithms. J. Symbolic Computation8, 51-99 (1989) · Zbl 0691.03003 · doi:10.1016/S0747-7171(89)80022-7
[34] Slagle, J. R.: Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity. J. ACM21, 622-642 (1974) · Zbl 0296.68092 · doi:10.1145/321850.321859
[35] Stickel, M.: Automated Deduction by Theory Resolution. J. Automated Reasoning1, 333-355 (1985) · Zbl 0616.68076 · doi:10.1007/BF00244275
[36] Taylor, W.: Equational Logic. Houston J. Math.5, 1-51 (1979) · Zbl 0421.08004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.