×

zbMATH — the first resource for mathematics

Abelian group unification algorithms for elementary terms. (English) Zbl 0555.68065
Automated theorem proving, Proc. Spec. Sess., 89th Meet. Am. Math. Soc., Denver/Colo. 1983, Contemp. Math. 29, 193-199 (1984).
[For the entire collection see Zbl 0545.00023.]
We describe a method of constructing Abelian group unification algorithms for elementary terms which uses any basis algorithms for the integer solutions of linear equations with integer coefficients. We illustrate the method with computer generated examples using two different algorithms.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)