Abstract
We report on the current state of our development of new decision algorithms for finitely presented Abelian groups (FPAG) based upon commutative-associative (C-A) term rewriting system methods. We show that the uniform word problem is solvable by a completion algorithm which generates Church-Rosser, Noetherian, C-A term rewriting systems. The raw result is theoretical, and few would contemplate implementing it directly because of the incredible amount of trash which would be generated. Much of this trash can be obviated by a different approach which achieves the same end. First, the uniform identity problem is solved by a modified C-A completion algorithm which generates Church-Rosser bases, and then the desired complete set can be computed directly from the Church-Rosser bases. Computer generated examples of the first part of this two part procedure are given. The second part is still under development. Our computer experiences suggest that Church-Rosser bases may often contain large numbers of rules, even for simple presentations. So we were naturally interested in finding better Church-Rosser basis algorithms. With some minor changes the method of [1966] can be used to generate Church-Rosser bases. The Smith basis algorithm appears promising because computer experiments suggest that the number of rules grows slowly. However, small examples with small coefficients can give rise to bases with very large coefficients which exceed machine capacity so we are not entirely satisfied with this approach.
This work was supported in part by NSF Grant MCS-8209143 and a Louisiana Tech University research grant.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ballantyne, A. and Lankford, D. New decision algorithms for finitely presented commutative semigroups. Louisiana Tech U., Math. Dept., report MTP-4, May 1979; J. Comput. Math. with Appl. 7 (1981), 159–165.
Bergman, G. The diamond lemma for ring theory. Advances in Math. 29 (1978), 178–218.
Buchberger, B. A criterion for detecting unnecessary reductions in the construction of Gröbner-bases. Lecture Notes in Comp. Sci. 72 (1979), Springer-Verlag, 3–21.
Cardoza, E. Computational complexity of the word problem for commutative semigroups. M.Sc. thesis, MIT, Cambridge, MA, Aug. 1978; and MAC Tech. Memo. 67, Oct. 1975.
Fages, F. (some results of Fages presented by J. P. Jouannaud at a GE term rewriting system conference, Sept. 1983)
Jacobson, N. Lectures in Abstract Algebra, II Linear Algebra, Van Nostrand, 1953.
Kapur, D. (comparison of computer generated examples at a GE term rewriting system conference, Sept. 1983)
Lankford, D. On proving term rewriting systems are Noetherian. Louisiana Tech U., Math. Dept., report MTP-3, May 1979.
Lankford, D. and Ballantyne, A. Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions. U. of Texas, Math. Dept., ATP project, report ATP-39, Aug. 1977.
Lankford, D. and Ballantyne, A. The refutation completeness of blocked permutative narrowing and resolution. Proc. Fourth Workshop on Automated Deduction, Austin, Texas, Feb. 1979, W. Joyner, ed., 168–174.
Mostowski, A. On the decidability of some problems in special class of groups. Fund. Math. LIX (1966), 123–135.
Mostowski, A. Computational algorithms for deciding some problems for nilpotent groups. Fund. Math. LIX (1966), 137–152.
Peterson, G. and Stickel, J. Complete sets of reductions for some equational theories. JACM 28,2 (Apr. 1981), 233–264.
Smith, D. A basis algorithm for finitely generated Abelian groups. Math. Algorithms 1,1 (Jan. 1966), 13–26.
Stickel, M. A complete unification algorithm for associative-commutative functions. Advance Papers of the Fourth International Conference on Artificial Intelligence, AI Lab, MIT, Aug. 1975, 71–76.
Reidemeister, K. Einführung in die kombinatorische Topologie, Braunschweig, 1932, 50–56.
Szmielew, W. Elementary properties of Abelian groups. Fund. Math. XLI (1954), 203–271.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lankford, D., Butler, G., Ballantyne, A. (1984). A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_8
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_8
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive