Algebraic Simplification

  • B. Buchberger
  • R. Loos
Part of the Computing Supplementum book series (COMPUTING, volume 4)


Some basic techniques for the simplification of terms are surveyed. In two introductory sections the problem of canonical algebraic simplification is formally stated and some elementary facts are derived that explain the fundamental role of simplification in computer algebra. In the subsequent sections two major groups of simplification techniques are presented: special techniques for simplifying terms over numerical domains and completion algorithms for simplification with respect to sets of equations. Within the first group canonical simplification algorithms for polynomials, rational expressions, radical expressions and transcendental expressions are treated (Sections 3–7). As examples for completion algorithms the Knuth-Bendix algorithm for rewrite rules and an algorithm for completing bases of polynomial ideals are described (Sections 8–11).


Canonical Form Computer Algebra System Polynomial Ideal Commutative Semigroup Critical Pair 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Aho, A., Sethi, R., Ullman, J.: Code Optimization and Finite Church-Rosser Systems. Proc. of Courant Comput. Sci. Symp. 5 (Rustin, R., ed.). Englewood Cliffs, N. J.: Prentice-Hall 1972.Google Scholar
  2. [2]
    Ayoub, C. W.: On Constructing Bases for Ideals in Polynomial Rings over the Integers. Pennsylvania State University, Univ. Park: Dept. Math. Rep. 8184 (1981).Google Scholar
  3. [3]
    Bachmair, L., Buchberger, B.: A Simplified Proof of the Characterization Theorem for Gröbner Bases. ACM SIGSAM Bull. 14/4, 29–34 (1980).MATHCrossRefGoogle Scholar
  4. [4]
    Ballantyne, A. M., Lankford, D. S.: New Decision Algorithms for Finitely Presented Commutative Semigroups. Comp. Math. Appl. 7, 159–165 (1981).MathSciNetCrossRefGoogle Scholar
  5. [5]
    Bergman, G. M.: The Diamond Lemma for Ring Theory. Adv. Math. 29, 178–218 (1978).MathSciNetCrossRefGoogle Scholar
  6. [6]
    Birkhoff, G.: On the Structure of Abstract Algebras. Proc. Cambridge Phil. Soc. 31, 433–454 (1935).CrossRefGoogle Scholar
  7. [7]
    Birkhoff, G., Lipson, J. D.: Heterogeneous Algebras. J. Comb. Theory 8, 115–133 (1970).MathSciNetMATHCrossRefGoogle Scholar
  8. [8]
    Boyer, R. S., Moore, J. S.: A Computational Logic. New York-London: Academic Press 1979.MATHGoogle Scholar
  9. [9]
    Brown, W. S.: Rational Exponential Expressions and a Conjecture Concerning π and e. Am. Math. Mon. 76, 28–34 (1969).MATHCrossRefGoogle Scholar
  10. [10]
    Brown, W. S.: On Euclid’s Algorithm and the Computation on Polynomial Greatest Common Divisor. J. ACM 18/4, 478–504 (1971).MATHCrossRefGoogle Scholar
  11. [11]
    Brown, W. S.: On Computing with Factored Rational Expressions. EUROSAM 1974, 26–34.Google Scholar
  12. [12]
    Buchberger, B.: An Algorithm for Finding a Basis for the Residue Class Ring of a ZeroDimensional Polynomial Ideal (German). Ph.D. Thesis, Math. Inst., Univ. of Innsbruck, Austria, 1965, andGoogle Scholar
  13. [12a]
    Buchberger, B.: An Algorithm for Finding a Basis for the Residue Class Ring of a ZeroDimensional Polynomial Ideal (German). Aequationes Math. 4/3, 374–383 (1970).MathSciNetMATHCrossRefGoogle Scholar
  14. [13]
    Buchberger, B.: A Criterion for Detecting Unnecessary Reductions in the Construction of Gröbner Bases. EUROSAM 1979, Lecture Notes in Computer Science, Vol. 72, pp. 3–21. Berlin-Heidelberg-New York: Springer 1979.Google Scholar
  15. [14]
    Bücken, H.: Reduktionssysteme und Wortproblem. Rhein.-Westf. Tech. Hochschule, Aachen: Inst. für Informatik, Rep. 3, 1979.Google Scholar
  16. [15]
    Burstall, R. M., Goguen, J. A.: Putting Theories Together to Make Specifications. Proc. 5th Internat. Joint Conf. on Artificial Intelligence 1977, 1045–1058.Google Scholar
  17. [16]
    Cardoza, E., Lipton, R., Meyer, A. R.: Exponential Space Complete Problems for Petri Nets and Commutative Semigroups. Conf. Record of the 8th Annual ACM Symp. on Theory of Computing, 50–54 (1976).Google Scholar
  18. [17]
    Caviness, B. F.: On Canonical Forms and Simplification, Ph.D. Diss., Pittsburgh, CarnegieMellon University, 1967,Google Scholar
  19. [17a]
    Caviness, B. F.: On Canonical Forms and Simplification, J. ACM 17/2, 385–396 (1970).MathSciNetMATHCrossRefGoogle Scholar
  20. [18]
    Caviness, B. F., Fateman, R.: Simplification of Radical Expressions. SYMSAC 1976, 329–338.Google Scholar
  21. [19]
    Caviness, B. F., Pollack, P. L., Rubald, C. M.: An Existence Lemma for Canonical Forms in Symbolic Mathematics. Inf. Process. Lett. 1, 45–46 (1971).MathSciNetMATHCrossRefGoogle Scholar
  22. [20]
    Church, A., Rosser, J. B.: Some Properties of Conversion. Trans. AMS 39, 472–482 (1936).MathSciNetCrossRefGoogle Scholar
  23. [21]
    Cohn, P. M.: Universal Algebra. New York: Harper and Row 1965.MATHGoogle Scholar
  24. [22]
    Collins, G. E.: The SAC-1 Polynomial System. Univ. of Wisconsin, Madison: Comput. Sci. Dept., Tech. Rep. 115, 1968.Google Scholar
  25. [23]
    Collins, G. E.: The Calculation of Multivariate Polynomial Resultants. J. ACM 18/4, 515–532 (1971).MATHCrossRefGoogle Scholar
  26. [24]
    Courcelle, B.: On Recursive Equations Having a Unique Solution. IRIA–Laboria Rep. 285 (1976).Google Scholar
  27. [25]
    Davenport, J.: On the Integration of Algebraic Functions. Univ. of Cambridge: Ph.D. Thesis. (Lecture Notes in Computer Science, Vol. 102.) Berlin-Heidelberg-New York: Springer 1981.Google Scholar
  28. [26]
    Davis, M.: Hilbert’s Tenth Problem is Unsolvable. Am. Math. Mon. 80/3, 233–269 (1973).MATHCrossRefGoogle Scholar
  29. [27]
    Davis, M., Putnam, H., Robinson, J.: The Decision Problem for Exponential Diophantine Equations. Ann. Math. 74, 425–436 (1961).MathSciNetMATHCrossRefGoogle Scholar
  30. [28]
    Dehn, M.: Über unendliche diskontinuierliche Gruppen. Math. Ann. 71, 116–144 (1911).MathSciNetCrossRefGoogle Scholar
  31. [29]
    Dershowitz, N.: A Note on Simplification Orderings. Inf. Process. Lett. 9/5, 212–215 (1979).MathSciNetMATHCrossRefGoogle Scholar
  32. [30]
    Dershowitz, N.: Orderings for Term-Rewriting Systems. Proc. 20th Symp. on Foundations of Comp. Sci. 1979, 123–131.Google Scholar
  33. [31]
    Dershowitz, N., Manna, Z.: Proving Termination with Multiset Ordering. Commun. ACM 22, 465–476 (1979).MathSciNetMATHCrossRefGoogle Scholar
  34. [32]
    Epstein, H. I.: Using Basis Computation to Determine Pseudo-Multiplicative Independence. SYMSAC 1976, 229 –237.Google Scholar
  35. [33]
    Evans, T.: The Word Problem for Abstract Algebras. J. London Math. Soc. 26, 64–71 (1951).MathSciNetMATHCrossRefGoogle Scholar
  36. [34]
    Fateman, R. J.: The User-Level Semantic Pattern Matching Capability in MACSYMA. Proc. SYMSAM 1971, 311–323.Google Scholar
  37. [35]
    Fateman, R. J.: Essays in Algebraic Simplification. Thesis, MIT, Project MAC 1972.Google Scholar
  38. [36]
    Fateman, R. J.: MACSYMA’s General Simplifier: Philosophy and Operation. MACSYMA 1979, 563–582.Google Scholar
  39. [37]
    Fateman, R. J.: Symbolic and Algebraic Computer Programming Systems. ACM SIGSAM Bull. 15/1, 21–32 (1981).MATHCrossRefGoogle Scholar
  40. [38]
    Fenichel, J.: An One-Line System for Algebraic Manipulation. Harvard Univ., Cambridge, Mass.: Ph.D. Thesis 1966.Google Scholar
  41. [39]
    Fitch, J. P.: An Algebraic Manipulator. Ph.D. Thesis, Univ. of Cambridge, 1971.Google Scholar
  42. [40]
    Fitch, J. P.: On Algebraic Simplification. Comput. J. 16/1, 23–27 (1973).MathSciNetMATHCrossRefGoogle Scholar
  43. [41]
    Foderaro, J. K.: Typesetting MACSYMA Equations. MACSYMA 1979, 345–361.Google Scholar
  44. [42]
    Gerhart, S. L., Musser, D. R., Thompson, D. H., Baker, D. A., Bates, R. L., Erickson, R. W., London, R. L., Taylor, D. G., Wile, D. S.: An Overview of AFFIRM: A Specification and Verification System. In: Information Processing 80 (Lavington, S. H., ed.), pp. 343–347. Amsterdam: North-Holland 1980.Google Scholar
  45. [43]
    Goguen, J. A.: How to Prove Algebraic Inductive Hypotheses without Induction, with Applications to the Correctness of Data Type Implementations. Proc. 5th Conf. on Aut. Deduction. Lecture Notes in Computer Science, Vol. 87, pp. 356–373. Berlin-Heidelberg-New York: Springer 1980.Google Scholar
  46. [44]
    Goguen, J. A., Thatcher, J. W., Wagner, E. G., Wright, J. B.: Abstract Data Types as Initial Algebras and Correctness of Data Representations. Proc. Conf. on Comput. Graphics, Pattern Recognition and Data Structure 1975, 89–93, Beverly Hills, California.Google Scholar
  47. [45]
    Griss, M. L: The Definition and Use of Datastructures in REDUCE. SYMSAC 1976, 53–59.Google Scholar
  48. [46]
    Hall, A. D.: Factored Rational Expressions in ALTRAN. EUROSAM 1974, 35–45.Google Scholar
  49. [47]
    Hearn, A. C.: A New REDUCE Model for Algebraic Simplification. SYMSAC 1976, 46–52.Google Scholar
  50. [48]
    Hearn, A. C.: Symbolic Computation: Past, Present, Future. Dept. of Comput. Sci., Univ. Utah, Salt Lake City 1978.Google Scholar
  51. [49]
    Henrici, P.: A Subroutine for Computations with Rational Numbers. J. ACM 3/1, 6–9 (1956).MathSciNetCrossRefGoogle Scholar
  52. [50]
    Hermann, G.: Die Frage der endlich vielen Schritte in der Theorie der Polynomideale. Math. Ann. 95, 736–788 (1926).MathSciNetMATHCrossRefGoogle Scholar
  53. [51]
    Hindley, R.: An Abstract Form of the Church-Rosser Theorem II: Applications. J. Symb. Logic 39/1, 1–21 (1974).MathSciNetMATHCrossRefGoogle Scholar
  54. [52]
    Hindley, R., Lercher, B., Seldin, J. P.: Introduction to Combinatory Logic. Cambridge: Camb. Univ. Press 1972.MATHGoogle Scholar
  55. [53]
    Huet, G. P.: Resolution d’équations dans des languages d’ordre 1, 2,…. ω. Ph.D. Thesis, University of Paris VII, 1976.Google Scholar
  56. [54]
    Huet, G.: A Complete Proof of the Knuth-Bendix Competion Algorithm. IRIA: Report (1979).Google Scholar
  57. [55]
    Huet, G. P.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. 18th IEEE Symp. on Foundat. of Comput. Sci., 30–45 (1977) and J. ACM 27/4, 797–821 (1980).MathSciNetMATHGoogle Scholar
  58. [56]
    Huet, G. P., Hullot, J. M.: Proofs by Induction in Equational Theories with Constructors. 21st IEEE Symp. on Foundations of Comput. Sci. 1980, 96–107.Google Scholar
  59. [57]
    Huet, G., Lankford, D. S.: On the Uniform Halting Problem for Term Rewriting Systems. IRIA: Rapp. Laboria 283, 1978.Google Scholar
  60. [58]
    Huet, G. P., Oppen, D. C.: Equations and Rewrite Rules: A Survey. Techn. Rep. CSL-111, SRI International, Stanford, 1980.Google Scholar
  61. [59]
    Hullot, J. M.: A Catalogue of Canonical Term Rewriting Systems. Stanford: SRI International Tech. Rep. CSL-113, 1980.Google Scholar
  62. [60]
    Jenks, R. D.: A Pattern Compiler. SYMSAC 1976, 60–65.Google Scholar
  63. [61]
    Johnson, S. C.: On the Problem of Recognizing Zero. J. ACM 18/4, 559–565 (1971).MATHCrossRefGoogle Scholar
  64. [62]
    Kapur, D., Musser, D. R., Stepanov, A. A.: Operators and Algebraic Structures. Schenectady, N.Y.: General Electric Automation and Control Laboratory, Report 81CRD 114 (1981).Google Scholar
  65. [63]
    King, J. C., Floyd, R. W.: An Interpretation Oriented Theorem Prover Over the Integers. J. Comput. Syst. Sci. 6/4, 305–323 (1972).MathSciNetMATHCrossRefGoogle Scholar
  66. [64]
    Kleiman, S. L.: Computing with Rational Expressions in Several Algebraically Dependent Variables. Columbia Univ., New York: Computing Science Techn. Report 42, 1966.Google Scholar
  67. [65]
    Knuth, D. E., Bendix, P. B.: Simple Word Problems in Universal Algebras. OXFORD 67, 263–298.Google Scholar
  68. [66]
    Korsvold, K.: An On-Line Algebraic Simplify Program. Stanford Univ.: Art. Int. Project Memorandum 37, 1965, andGoogle Scholar
  69. [66a]
    Korsvold, K.: An On-Line Algebraic Simplify Program. Comm. ACM 9, 553 (1966).Google Scholar
  70. [67]
    Lafferty, E. L.: Hypergeometric Function Reduction–an Adventure in Pattern Matching. MACSYMA 1979, 465–481.Google Scholar
  71. [68]
    Lang, S.: Transcendental Numbers and Diophantine Approximations. Bull. AMS 77/5, 635–677 (1971).MATHCrossRefGoogle Scholar
  72. [69]
    Lankford, D. S.: Canonical Algebraic Simplification. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-25, 1975.Google Scholar
  73. [70]
    Lankford, D. S.: Canonical Inference. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-32, 1975.Google Scholar
  74. [71]
    Lankford, D. S.: Research in Applied Equational Logic. Louisiana Tech. Univ., Ruston: Math. Dept., MTP-15, 1980.Google Scholar
  75. [72]
    Lankford, D. S.: A Simple Explanation of Inductionless Induction. Louisiana Tech. Univ., Ruston: Math. Dept., MTP-14, 1981.Google Scholar
  76. [73]
    Lankford, D. S., Ballantyne, A. M.: Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-35, 1977.Google Scholar
  77. [74]
    Lankford, D. S., Ballantyne, A. M.: Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Permutative Reductions. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-37, 1977.Google Scholar
  78. [75]
    Lankford, D. S., Ballantyne, A. M.: Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets of Commutative-Associative Reductions. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-39, 1977.Google Scholar
  79. [76]
    Lauer, M.: Canonical Representatives for Residue Classes of a Polynomial Ideal. SYMSAC 1976, 339–345.Google Scholar
  80. [77]
    Lausch, H., Nöbauer, W.: Algebra of Polynomials. Amsterdam: North-Holland 1973.MATHGoogle Scholar
  81. [78]
    Lichtenberger, F.: PL/ADT: A System for Using Algebraically Specified Abstract Data Types in PL/I (German). Ph.D. Thesis, Math. Inst., Univ. of Linz, Austria, 1980.Google Scholar
  82. [79]
    Loos, R.: Toward a Formal Implementation of Computer Algebra. EUROSAM 1974, 9–16.Google Scholar
  83. [80]
    Loos, R.: Algorithmen und Datenstrukturen I: Abstrakte Datentypen. Univ. Karlsruhe, Federal Republic of Germany: Lecture Notes, 1980.Google Scholar
  84. [81]
    Loos, R.: Term Reduction Systems and Algebraic Algorithms. Proc. 5th GI Workshop on Artif. Intell., Bad Honnef 1981, Informatik Fachberichte 47, 214–234 (1981).Google Scholar
  85. [82]
    Loveland, D. W., Shostak, R. E.: Simplifying Interpreted Formulas. 5th Conf. on Automated Deduction, Les Arces, France, 1980. Lecture Notes in Computer Science, Vol. 87, pp. 97–109. Berlin-Heidelberg-New York: Springer 1980.CrossRefGoogle Scholar
  86. [83]
    Luckham, D. C., German, S. M., Henke, F. W., Karp, R. A., Milne, P. W., Oppen, D. C., Polak, W., Scherlis, W. L.: Stanford PASCAL Verifier User Manual. Stanford Univ.: Comput. Sci. Dept., Rep. STAN-CS-79-731, 1979.Google Scholar
  87. [84]
    Manin, Y. I.: A Course in Mathematical Logic. Berlin-Heidelberg-New York: Springer 1977.MATHGoogle Scholar
  88. [85]
    Manna, Z., Ness, S.: On the Termination of Markov Algorithms. Third Hawaii International Conference on System Sciences 1970, 789–792.Google Scholar
  89. [86]
    Martelli, A., Montanari, U.: An Efficient Unification Algorithm. Unpublished Report (1979).Google Scholar
  90. [87]
    Martin, W. A.: Computer Input/Output of Mathematical Expressions. SYMSAM 1971, 78–89.Google Scholar
  91. [88]
    Martin, W. A.: Determining the Equivalence of Algebraic Expressions by Hash Coding. SYMSAM 1971, 305–310.Google Scholar
  92. [89]
    Matiyasevic, J.: Diophantine Representation of Recursively Enumerable Predicates. Proc. Second Scandinavian Logic Symp. Amsterdam: North-Holland 1970.Google Scholar
  93. [90]
    Mayr, E. W., Meyer, A. R.: The Complexity of the Word Problems for Commutative Semigroups and Polynomial Ideals. M.I.T.: Lab. Comput. Sci. Rep. LCS/TM-199 (1981).Google Scholar
  94. [91]
    McDonald, I. D.: A Computer Application to Finite p-Groups. J. Aust. Math. Soc. 17, 102–112 (1974).CrossRefGoogle Scholar
  95. [92]
    Möller, H. M.: Mehrdimensionale Hermite-Interpolation und numerische Integration. Math. Z. 148, 107–118 (1976).MathSciNetMATHCrossRefGoogle Scholar
  96. [93]
    Moses, J.: Symbolic Integration. Ph.D. Thesis, Cambridge, Mass., M.I.T., Math. Dept., Rep. MAC-47, 1967.Google Scholar
  97. [94]
    Moses, J.: Algebraic Simplification: A Guide for the Perplexed. SYMSAM 1971, 282 –304 and Commun. ACM 14, 527–537 (1971).MathSciNetMATHGoogle Scholar
  98. [95]
    Musser, D. R.: Algorithms for Polynomial Factorization. Univ. of Wisconsin, Madison: Ph.D. Thesis, Techn. Rep. 134, 1971.Google Scholar
  99. [96]
    Musser, D. R.: A Data Type Verification System Based on Rewrite Rules. USC Information Science Institute, Marina del Rey, Calif.: 1977.Google Scholar
  100. [97]
    Musser, D. R.: Convergent Sets of Rewrite Rules for Abstract Data Types. Information Sciences Institute: Report 1978.Google Scholar
  101. [98]
    Musser, D. R.: On Proving Inductive Properties of Abstract Data Types. Seventh ACM Symp. on Principles of Programming Languages 1980, 154–162.Google Scholar
  102. [99]
    Newman, M. F.: Calculating Presentations for Certain Kinds of Quotient Groups. SYMSAC 1976, 2–8.Google Scholar
  103. [100]
    Newman, M. H. A.: On Theories with a Combinatorial Definition of “Equivalence”. Ann. Math. 43/2, 223–243 (1942).MATHCrossRefGoogle Scholar
  104. [101]
    O’Donnell, M.: Computing in Systems Described by Equations. Lecture Notes in Computer Science, Vol. 58. Berlin-Heidelberg-New York: Springer 1977.MATHCrossRefGoogle Scholar
  105. [102]
    Oldehoeft, A.: Analysis of Constructed Mathematical Responses by Numeric Tests for Equivalence. Proc. ACM 24th Nat. Conf., 117–124 (1969).Google Scholar
  106. [103]
    Paterson, M. S., Wegmann, M. N.: Linear Unification. J. Comput. Syst. Sci. 16, 158–167 (1978).MATHCrossRefGoogle Scholar
  107. [104]
    Pavelle, R., Rothstein, M., Fitch, J.: Computer Algebra. Preprint, Scientific American 1981.Google Scholar
  108. [105]
    Peterson, G. E., Stickel, M. E.: Complete Set of Reductions for Some Equational Theories. J. ACM 28/2, 233–264 (1981).MathSciNetMATHCrossRefGoogle Scholar
  109. [106]
    Plaisted, D.: Well-Founded Orderings for Proving Termination of Systems of Rewrite Rules. Univ. of Illinois, Urbana-Champaign: Rep. 78–932, 1978.Google Scholar
  110. [107]
    Plaisted, D.: A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems. Univ. of Illinois, Urbana-Champaign: Rep. 78–943, 1978.Google Scholar
  111. [108]
    Plotkin, G.: Building-In Equational Theories. Machine-Intelligence 7, 73 –90 (1972).MathSciNetMATHGoogle Scholar
  112. [109]
    Pohst, M., Yun, D. Y. Y.: On Solving Systems of Algebraic Equations Via Ideal Bases and Elimination Theory. SYMSAC 1981, 206 –211.Google Scholar
  113. [110]
    Polak, W.: Program Verification at Stanford: Past, Present, Future. Stanford University: Comput. Syst. Lab., Rep. 1981.Google Scholar
  114. [111]
    Raulefs, P., Siekmann, J., Szabó, P., Unvericht, E.: A Short Survey on the State of the Art in Matching and Unification Problems. SIGSAM Bull. 13/2, 14–20 (1979).CrossRefGoogle Scholar
  115. [112]
    Reynolds, J. C.: Reasoning About Arrays. Commun. ACM 22/5, 290 –299 (1979).MATHCrossRefGoogle Scholar
  116. [113]
    Richardson, D.: Some Unsolvable Problems Involving Elementary Functions of a Real Variable. J. Symb. Logic 33, 511–520 (1968).Google Scholar
  117. [114]
    Richardson, D.: Solution of the Identity Problem for Integral Exponential Functions. Math. Logik Grundlagen Math. 15, 333–340 (1969).MathSciNetMATHCrossRefGoogle Scholar
  118. [115]
    Richter, M. M., Kemmenich, S.: Reduktionssysteme und Entscheidungsverfahren. Rhein.Westf. Tech. Hochschule, Aachen: Inst. f. Informatik, Rep. 4, 1980.Google Scholar
  119. [116]
    Risch, R. H.: The Problem of Integration in Finite Terms. Trans. AMS 139, 167–189 (1969).MathSciNetMATHCrossRefGoogle Scholar
  120. [117]
    Robinson, J. A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12, 23–41 (1965).MATHCrossRefGoogle Scholar
  121. [118]
    Robinson, J. A.: Computational Logic: The Unification Computation. Machine Intelligence 6, 63–72. New York: Edinb. Univ. Press 1971.Google Scholar
  122. [119]
    Rogers, H.: Theory of Recursive Functions and Effective Computability. New York: McGrawHill 1967.MATHGoogle Scholar
  123. [120]
    Rosen, B. K.: Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM 20/1, 160–187 (1973).MATHCrossRefGoogle Scholar
  124. [121]
    Schaller, S.: Algorithmic Aspects of Polynomial Residue Class Rings. Ph.D. Thesis, Comput. Sci. Tech., University of Wisconsin, Madison, Rep. 370, 1979.Google Scholar
  125. [122]
    Schrader, R.: Zur konstruktiven Idealtheorie. Dipl. Thesis, Math. Inst., Univ. of Karlsruhe, Federal Republic of Germany 1976.Google Scholar
  126. [123]
    Seidenberg, A.: Constructions in Algebra. Trans. AMS 197, 273–313 (1974).MathSciNetMATHCrossRefGoogle Scholar
  127. [124]
    Sethi, R.: Testing for the Church-Rosser Property. J. ACM 21/4, 671–679 (1974),MathSciNetMATHCrossRefGoogle Scholar
  128. [124a]
    Sethi, R.: Testing for the Church-Rosser Property. J. ACM 22/3, 424 (1975).MathSciNetCrossRefGoogle Scholar
  129. [125]
    Shtokhamer, R.: Simple Ideal Theory: Some Applications to Algebraic Simplifiication. Univ. of Utah, Salt Lake City: Tech. Rep. UCP-36, 1975.Google Scholar
  130. [126]
    Shtokhamer, R.: A Canonical Form of Polynomials in the Presence of Side Relations. Technion, Haifa: Phys. Dept., Rep. 25, 1976.Google Scholar
  131. [127]
    Shtokhamer, R.: Attempts in Local Simplification of Non-Nested Radicals. SIGSAM Bull. 11/1, 20–21 (1977).MATHCrossRefGoogle Scholar
  132. [128]
    Spear, D.: A Constructive Approach to Commutative Ring Theory. MACSYMA 1977, 369–376.Google Scholar
  133. [129]
    Staples, J.: Church-Rosser Theorems for Replacement Systems. Algebra and Logic (Crossley, J., ed.), Lecture Notes in Mathematics, Vol. 450, pp. 291–307. Berlin-Heidelberg-New York: Springer 1975.Google Scholar
  134. [130]
    Stickel, M. E., Peterson, G. E.: Complete Sets of Reductions for Equational Theories with Complete Unification Algorithm. Univ. of Arizona: Dept. Comp. Sci. 1977.Google Scholar
  135. [131]
    Stoutemyer, D. R.: Qualitative Analysis of Mathematical Expressions Using Computer Symbolic Mathematics. SYMSAC 1976, 97–104.Google Scholar
  136. [132]
    Stoutemyer, D. R.: Automatic Simplification for the Absolute Value Function and its Relatives. ACM SIGSAM Bull. 10/4, 48–49 (1976).CrossRefGoogle Scholar
  137. [133]
    Suzuki, N., Jefferson, D.: Verification Decidability of Presburger Array Programs. J. ACM 27/1, 191–205 (1980).MathSciNetMATHCrossRefGoogle Scholar
  138. [134]
    Szekeres, G.: A Canonical Basis for the Ideals of a Polynomial Domain. Am. Math. Mon. 59/6, 379–386 (1952).MathSciNetMATHCrossRefGoogle Scholar
  139. [135]
    Tobey, R. G.: Experience with FORMAC Algorithm Design. Commun. ACM 9, 589–597 (1966).MATHCrossRefGoogle Scholar
  140. [136]
    Todd, J. A., Coxeter, H. S. M.: A Practical Method for Enumerating Cosets of a Finite Abstract Group. Proc. Edinb. Math. Soc. (2) 5, 26–34 (1936).MATHCrossRefGoogle Scholar
  141. [137]
    Trinks, W.: Über B. Buchbergers Verfahren, Systeme algebraischer Gleichungen zu lösen. J. Number Theory 10/4, 475–488 (1978).MathSciNetMATHCrossRefGoogle Scholar
  142. [138]
    Trotter, P. G.: Ideals in Z[x, y]. Acta Math. Acad. Sci. Hungar. 32 (1–2), 63–73 (1978).MathSciNetMATHCrossRefGoogle Scholar
  143. [139]
    Winkler, F., Buchberger, B., Lichtenberger, F., Rolletschek, H.: An Algorithm for Constructing Canonical Bases (Gröbner-Bases) for Polynomial Ideals. (Submitted.)Google Scholar
  144. [140]
    Yun, D. Y. Y., Stoutemyer, R. D.: Symbolic Mathematical Computation. Encyclopedia of Computer Science and Technology (Belzer, J., Holzman, A. G., Kent, A., eds.), Vol. 15, pp. 235–310. New York-Basel: Marcel Dekker 1980.Google Scholar
  145. [141]
    Zacharias, G.: Generalized Gröbner Bases in Commutative Polynomial Rings. Bachelor Thesis, Dept. Comput. Sci., M.I.T., 1978.Google Scholar
  146. [142]
    Zippel, R. E. B.: Simplification of Radicals with Applications to Solving Polynomial Equations. Cambridge, Mass.: M.I.T., Dept. of Electrical Engineering and Computer Science, Master’s Thesis, 1977.Google Scholar

Copyright information

© Springer-Verlag Wien 1982

Authors and Affiliations

  • B. Buchberger
    • 1
  • R. Loos
    • 2
  1. 1.Institut für MathematikJohannes-Kepler-Universität LinzLinzAustria
  2. 2.Institut für Informatik IUniversität KarlsruheKarlsruheFederal Republic of Germany

Personalised recommendations