Abstract
A new approach based on computing the Gröbner basis of polynomial ideals is developed for solving word problems and unification problems for finitely presented commutative algebras. This approach is simpler and more efficient than the approaches based on generalizations of the Knuth-Bendix completion procedure to handle associative and commutative operators. It is shown that (i) the word problem over a finitely presented commutative ring with unity is equivalent to the polynomial equivalence problem modulo a polynomial ideal over the integers, (ii) the unification problem for linear forms is decidable for finitely presented commutative rings with unity, (iii) the word problem and unification problem for finitely presented boolean polynomial rings are co-NP-complete and co-NP-hard respectively, and (iv) the set of all unifiers of two forms over a finitely presented abelian group can be computed in polynomial time. Examples and results of algorithms based on the Gröbner basis computation are also reported.
This work was done when Kandri-Rody was a graduate student at Rensselaer Polytechnic Institute, Troy, NY.
Partially supported by the National Science Foundation grant MCS-82-11621.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
7. References
Angarsson, S., Kandri-Rody, A., Kapur, D., Narendran, P., and Saunders, B.D., “The Complexity of Testing whether a Polynomial Ideal is Nontrivial,” Proceedings of the Third MACSYMA User's Conference, Schenectady, NY, July, 1984, pp. 452–458.
Ballantyne, A.M., and Lankford, D.S., “New Decision Algorithms for Finitely Presented Commutative Semigroups,” Computer and Mathematics with Applications Vol. 7 pp. 159–165, 1981.
Buchberger, B., An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Polynomial Ideal (in German), Ph.D. Thesis, Univ. of Innsbruck, Austria, Math., Inst., 1965.
Buchberger, B., “A Critical-Pair/Completion Algorithm in Reduction Rings,” Proc. Logic and Machines: Decision Problems and Complexity, (eds. by E. Borger, G. Hasenjaeger, D. Rodding), Spring LNCS 171, pp 137–161, 1984.
Buchberger, B., and Loos, R., “Algebraic Simplification,” in Computer Algebra: Symbolic and Algebraic Computation (Eds. B. Buchberger, G.E. Collins and R. Loos), Computing Suppl. 4 (1982), Springer Verlag, New York, pp. 11–43.
Chou, T.J., and Collins, G.E., “Algorithms for the Solutions of Systems of Linear Diophantine Equations,” Siam J. Comput. 11 (1982), pp. 687–708.
Garey, M.R. and Johnson, D.S., Computers and Intractability, W.H. Freeman, 1979.
Hsiang, J., Topics in Theorem Proving and Program Synthesis, Ph.D. Thesis, University of Illinois, Urbana-Champagne, July 1983.
Huet, G., “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” JACM, Vol. 27, No. 4, October 1980, pp. 797–821. on Automata, Languages, and Programming (1983), Spain.
Kandri-Rody, A., and Kapur, D., “Computing the Gröbner Basis of a Polynomial Ideal over Integers,” Proceedings of the Third MACSYMA Users' Conference, Schenectady, NY, July 1984, pp. 436–451.
Kandri-Rody, A., and Kapur, D., “Algorithms for Computing the Gröbner Bases of Polynomial Ideals over Various Euclidean Rings,” Proceedings of the EUROSAM, '84, Cambridge, England, July 1984.
Kandri-Rody, A., and Kapur, D., "An Algorithm for Computing the Gröbner Basis of a Polynomial Ideal over a Euclidean Ring,” General Electric Corporate Research and Development Report 84CRD045, April, 1984; Revised, December, 1984.
Kannan, R., and Bachem, A., “Prolynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix,” Siam J. Comput. 8 (1979), pp. 499–507.
Kapur, D., and Narendran, P., “An Equational Approach to Theorem Proving in First-Order Predicate Calculus,” to appear in the Proc. of the IJCAI-85, Los Angeles, August, 1985.
Knuth, D.E. and Bendix, P.B., “Simple Word Problems in Universal Algebras,” in Computational Problems in Abstract Algebras. (Ed. J. Leech), Pergamon Press, 1970, pp. 263–297.
Lankford, D.S., and Ballantyne, A.M., “Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets of Commutative-Associative Reductions,” Automatic Theorem Proving Project, Dept. of Math. and Computer Science, University of Texas, Austin, TX 78712, Report ATP-39, August 1977.
Lankford, D.S., Butler, G., and Brady, B., “Abelian Group Unification Algorithms for Elementary Terms,” Proceedings of a NSF Workshop on the Rewrite Rule Laboratory, September 6–9, 1983, General Electric Report, April, 1984.
Lankford, D.S., Butler, G., and Ballantyne, A.M., “A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups,” 7th Conference on Automated Deduction, Springer Verlag LNCS 170 (ed. R.E. Shostak), NAPA Valley, Calif., May, 1984, pp. 128–141.
Lankford, D.S, and Butler, G., “On the Foundations of Applied Equational Logic,” Talk Given at General Electric Research and Development Center, Schenectady, NY, Feb., 1984.
Lauer, M., “Canonical Representatives for Residue Classes of a Polynomial Ideal,” SYMSAC 1976, pp. 339–345.
Le Chenadec, P., “Canonical Forms in Finitely Presented Algebras,” 7th International Conf. on Automated Deduction, Springer Verlag LNCS 170 (ed. R.E. Shostak), Napa Valley, Calif, May, 1984, pp. 142–165.
Matijasevitch, J., “Enumerable Sets are Diophantine,” Dokl. Akad. Nauk. SSSR 191 (1970), pp. 279–282.
Peterson, G.L., and Stickel, M.E., “Complete Sets of Reductions for Some Equational Theories,” JACM 28 (1981), pp. 233–264.
Schaller, S., Algorithmic Aspects of Polynomial Residue Class Rings, Ph.D. Thesis, Computer Science Tech. Report 370, University of Wisconsin, Madison, 1979.
Stickel, M.E., “A Unification Algorithm for Associative-Commutative Functions,” JACM 28 (1980), pp. 423–434.
Szmielew, W., “Elementary Properties of Abelian Groups,” Fund. Math. XLI (1954), pp. 203–271.
van der Waerden, B.L., Modern Algebra, Vols. I and II, Fredrick Ungar Publishing Co., New York, 1966.
Zacharias, G., Generalized Grobner Bases in Commutative Polynomial Rings, Bachelor Thesis, Lab. for Computer Science, MIT, 1978.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kandri-Rody, A., Kapur, D., Narendran, P. (1985). An ideal-theoretic approach to word problems and unification problems over finitely presented commutative algebras. In: Jouannaud, JP. (eds) Rewriting Techniques and Applications. RTA 1985. Lecture Notes in Computer Science, vol 202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15976-2_17
Download citation
DOI: https://doi.org/10.1007/3-540-15976-2_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15976-6
Online ISBN: 978-3-540-39679-6
eBook Packages: Springer Book Archive