×

zbMATH — the first resource for mathematics

Unification in commutative theories. (English) Zbl 0689.68039
Summary: A general framework for unification in “commutative“ theories is investigated which is based on a categorical reformulation of theory unification. 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.

MSC:
68W30 Symbolic computation and algebraic computation
68Q65 Abstract data types; algebraic specification
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baader, F., Unification in varieties of idempotent semigroups, () · Zbl 0624.20039
[2] Baader, F.; Büttner, W., Unification in commutative idempotent monoids, Tcs, 56, (1988) · Zbl 0658.68108
[3] Büttner, W., Unification in the data structure multiset, J. automated reasoning, 2, (1986)
[4] Clausen, M.; Fortenbacher, A., Efficient solution of linear Diophantine equations, Jsc, (1988), this issue
[5] Clifford, A.H.; Preston, G.B., The algebraic theory of semigroups, Vol. 2, (1967), AMS Mathematical Surveys 7 · Zbl 0178.01203
[6] Cohn, P.M., ()
[7] Fages, F., Associative-commutative unification, (), Springer Lec. Notes Comp. Sci. 170 · Zbl 0547.03012
[8] Fages, F.; Huet, G., Complete sets of unifiers and matchers in equational theories, Tcs, 43, (1986) · Zbl 0615.03002
[9] Fortenbacher, A., An algebraic approach to unification under associativity and commutativity, (), Springer Lec. Notes Comp. Sci. 202 · Zbl 0581.68029
[10] Freyd, P., ()
[11] Grätzer, G., ()
[12] Herold, A., Combination of unification algorithms in equational theories, () · Zbl 0679.03002
[13] Herrlich, H.; Strecker, G.E., ()
[14] Huet, G., An algorithm to generate the basis of solutions to homogeneous Diophantine equations, Information processing letters, 7, (1978) · Zbl 0377.10011
[15] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM, 27, (1980) · Zbl 0458.68007
[16] Jacobson, N., ()
[17] Jouannaud, J.P., Confluent and coherent equational term rewriting systems, applications to proofs in abstract data types, (), Springer Lec Notes Comp. Sci. 159 · Zbl 0522.68013
[18] Jouannaud, J.P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. comp., 15, (1986) · Zbl 0665.03005
[19] Knuth, D.E., ()
[20] Kurosh, A.G., ()
[21] Lambert, J-L., Une borne pour LES générateurs des solutions entières positives ďune équation diophantienne linéaire, Crasp, 305, (1987)
[22] Lankford, D.; Butler, G.; Brady, B., Abelian group unification algorithms for elementary terms, Contemporary mathematics, 29, (1984) · Zbl 0555.68065
[23] Lawvere, F.W., Functional semantics of algebraic theories, () · Zbl 0119.25901
[24] Livesey, M.; Siekmann, J., Unification in sets and multisets, ()
[25] Makanin, G.S., The problem of solvability of equations in a free semigroup, Mat. sbornik, 103, (1977), English transl. in Math USSR Sbornik\bf32 (1977) · Zbl 0379.20046
[26] Nash-Williams, C.St.J.A., On well-quasi-ordering finite trees, Proc. Cambridge philos. soc., 59, (1963) · Zbl 0122.25001
[27] Nevins, A.J., A human oriented logic for automated theorem proving, J. ACM, 21, (1974) · Zbl 0332.68061
[28] Niven, I.; Zuckerman, H.S., ()
[29] Peterson, G.; Stickel, M., Complete sets of reductions for some equational theories, J. ACM, 28, (1981) · Zbl 0479.68092
[30] Plotkin, G., Building in equational theories, Machine intelligence, 7, (1972) · Zbl 0262.68036
[31] Rydeheard, D.E.; Burstall, R.M., A categorical unification algorithm, (), Springer Lec. Notes Comp. Sci. 240 · Zbl 0616.68016
[32] Siekmann, J., Universal unification, () · Zbl 0584.68050
[33] Slage, J.R., Automated theorem proving for theories with simplifiers, commu-tativity and associativity, J. ACM, 21, (1974)
[34] Stickel, M., A unification algorithm for associative-commutative functions, J. ACM, 28, (1981) · Zbl 0462.68075
[35] Stickel, M., Automated deduction by theory resolution, J. automated reasoning, 1, (1985) · Zbl 0616.68076
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.