Advertisement

Algebraic Simplification

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

Abstract

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).

Keywords

Computer Algebra System Polynomial Ideal Critical Pair Ground Term Abstract Data Type 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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 Charaeterization 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).MATHMathSciNetCrossRefGoogle 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 Zero- Dimensional Polynomial Ideal (German). Ph.D. Thesis, Math. Inst., Univ. of Innsbruck, Austria, 1965, and Aequationes Math. 4/3, 374–383 (1970).Google Scholar
  13. [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
  14. [14]
    Bücken, H.: Reduktionssysteme und Wortproblem. Rhein.-Westf. Tech. Hochschule, Aachen: Inst, für Informatik, Rep. 3, 1979.Google Scholar
  15. [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
  16. [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
  17. [17]
    Caviness, B. F.: On Canonical Forms and Simplification, Ph.D. Diss., Pittsburgh, Carnegie- Mellon University, 1967, and J. ACM 17/2, 385–396 (1970).Google Scholar
  18. [18]
    Caviness, B. F., Fateman, R.: Simplification of Radical Expressions. SYMSAC 1976, 329–338.Google Scholar
  19. [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).MATHMathSciNetCrossRefGoogle Scholar
  20. [20]
    Church, A., Rosser, J. B.: Some Properties of Conversion. Trans. AMS 39, 472–482 (1936).MathSciNetCrossRefGoogle Scholar
  21. [21]
    Cohn, P. M.: Universal Algebra. New York: Harper and Row 1965.MATHGoogle Scholar
  22. [22]
    Collins, G. E.: The SAC-1 Polynomial System. Univ. of Wisconsin, Madison: Comput. Sci. Dept., Tech. Rep. 115, 1968.Google Scholar
  23. [23]
    Collins, G. E.: The Calculation of Multivariate Polynomial Resultants. J. ACM 18/4, 515–532 (1971).MATHCrossRefGoogle Scholar
  24. [24]
    Courcelle, B.: On Recursive Equations Having a Unique Solution. IRIA-Laboria Rep. 285 (1976).Google Scholar
  25. [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.MATHGoogle Scholar
  26. [26]
    Davis, M.: Hilbert’s Tenth Problem is Unsolvable. Am. Math. Mon. 80/3, 233–269 (1973).MATHCrossRefGoogle Scholar
  27. [27]
    Davis, M., Putnam, H., Robinson, J.: The Decision Problem for Exponential Diophantine Equations. Ann. Math. 74, 425–436 (1961).MATHMathSciNetCrossRefGoogle Scholar
  28. [28]
    Dehn, M.: Über unendliche diskontinuierliche Gruppen. Math. Ann. 71, 116–144 (1911).MathSciNetCrossRefGoogle Scholar
  29. [29]
    Dershowitz, N.: A Note on Simplification Orderings. Inf. Process. Lett. 9/5, 212–215 (1979).MATHMathSciNetCrossRefGoogle Scholar
  30. [30]
    Dershowitz, N.: Orderings for Term-Rewriting Systems. Proc. 20th Symp. on Foundations of Comp. Sci. 1979, 123–131.Google Scholar
  31. [31]
    Dershowitz, N., Manna, Z.: Proving Termination with Multiset Ordering. Commun. ACM 22, 465–476 (1979).MATHMathSciNetCrossRefGoogle Scholar
  32. [32]
    Epstein, H. I.: Using Basis Computation to Determine Pseudo-Multiplicative Independence. SYMSAC 1976, 229–237.CrossRefGoogle Scholar
  33. [33]
    Evans, T.: The Word Problem for Abstract Algebras. J. London Math. Soc. 26, 64–71 (1951).MATHMathSciNetCrossRefGoogle Scholar
  34. [34]
    Fateman, R. J.: The User-Level Semantic Pattern Matching Capability in MACSYMA. Proc. SYMSAM 1971, 311–323.Google Scholar
  35. [35]
    Fateman, R. J.: Essays in Algebraic Simplification. Thesis, MIT, Project MAC 1972.Google Scholar
  36. [36]
    Fateman, R. J.: MACSYMA’s General Simplifier: Philosophy and Operation. MACSYMA 1979, 563–582.Google Scholar
  37. [37]
    Fateman, R. J.: Symbolic and Algebraic Computer Programming Systems. ACM SIGSAM Bull. 15/1, 21–32 (1981).MATHCrossRefGoogle Scholar
  38. [38]
    Fenichel, J.: An One-Line System for Algebraic Manipulation. Harvard Univ., Cambridge, Mass.: Ph.D. Thesis 1966.Google Scholar
  39. [39]
    Fitch, J. P.: An Algebraic Manipulator. Ph.D. Thesis, Univ. of Cambridge, 1971.Google Scholar
  40. [40]
    Fitch, J. P.: On Algebraic Simplification. Comput. J. 16/1, 23–27 (1973).MATHMathSciNetCrossRefGoogle Scholar
  41. [41]
    Foderaro, J. K.: Typesetting MACSYMA Equations. MACSYMA 1979, 345–361.Google Scholar
  42. [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
  43. [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
  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
  45. [45]
    Griss, M. L: The Definition and Use of Datastructures in REDUCE. SYMSAC 1976, 53–59.CrossRefGoogle Scholar
  46. [46]
    Hall, A. D.: Factored Rational Expressions in ALTRAN. EUROSAM 1974, 35–45.Google Scholar
  47. [47]
    Hearn, A. C.: A New REDUCE Model for Algebraic Simplification. SYMSAC 1976, 46–52.CrossRefGoogle Scholar
  48. [48]
    Hearn, A. C.: Symbolic Computation: Past, Present, Future. Dept. of Comput. Sci., Univ. Utah, Salt Lake City 1978.Google Scholar
  49. [49]
    Henrici, P.: A Subroutine for Computations with Rational Numbers. J. ACM 3/1,6–9 (1956).MathSciNetCrossRefGoogle Scholar
  50. [50]
    Hermann, G.: Die Frage der endlich vielen Schritte in der Theorie der Polynomideale. Math. Ann. 95, 736–788 (1926).MATHMathSciNetCrossRefGoogle Scholar
  51. [51]
    Hindley, R.: An Abstract Form of the Church-Rosser Theorem II: Applications. J. Symb. Logic 39/1, 1–21 (1974).MATHMathSciNetCrossRefGoogle Scholar
  52. [52]
    Hindley, R., Lercher, B., Seldin, J. P.: Introduetion to Combinatory Logic. Cambridge: Camb. Univ. Press 1972.Google Scholar
  53. [53]
    Huet, G. P.: Resolution d’equations dans des languages d’ordre 1, 2,…,ω. Ph.D. Thesis, University of Paris VII, 1976.Google Scholar
  54. [54]
    Huet, G.: A Complete Proof of the Knuth-Bendix Competion Algorithm. IRIA: Report (1979).Google Scholar
  55. [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).Google Scholar
  56. [56]
    Huet, G. P., Hullot, J. M.: Proofs by Induction in Equational Theories with Constructors. 2Ist IEEE Symp. on Foundations of Comput. Sci. 1980, 96–107.Google Scholar
  57. [57]
    Huet, G., Lankford, D. S.: On the Uniform Halting Problem for Term Rewriting Systems. IRIA: Rapp. Laboria 283, 1978.Google Scholar
  58. [58]
    Huet, G. P., Oppen, D. C.: Equations and Rewrite Rules: A Survey. Techn. Rep. CSL-111, SRI International, Stanford, 1980.Google Scholar
  59. [59]
    Hullot, J. M.: A Catalogue of Canonical Term Rewriting Systems. Stanford: SRI International Tech. Rep. CSL-113, 1980.Google Scholar
  60. [60]
    Jenks, R. D.: A Pattern Compiler. SYMSAC 1976, 60–65.CrossRefGoogle Scholar
  61. [61]
    Johnson, S. C.: On the Problem of Recognizing Zero. J. ACM 18/4, 559–565 (1971).MATHCrossRefGoogle Scholar
  62. [62]
    Kapur, D., Musser, D. R., Stepanov, A. A.: Operators and Algebraic Structures. Schenectady, N.Y.: General Electric Automation and Control Laboratory, Report 81CRD114 (1981).Google Scholar
  63. [63]
    King, J. C., Floyd, R. W.: An Interpretation Oriented Theorem Prover Over the Integers. J. Comput. Syst. Sci. 6/4, 305–323 (1972).MATHMathSciNetCrossRefGoogle Scholar
  64. [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
  65. [65]
    Knuth, D. E., Bendix, P. B.: Simple Word Problems in Universal Algebras. OXFORD 67, 263–298.Google Scholar
  66. [66]
    Korsvold, K.: An On-Line Algebraic Simplify Program. Stanford Univ.: Art. Int. Project Memorandum 37, 1965, and Comm. ACM 9, 553 (1966).Google Scholar
  67. [67]
    Lafferty, E. L.: Hypergeometric Function Reduction-an Adventure in Pattern Matching. MACSYMA 1979, 465–481.Google Scholar
  68. [68]
    Lang, S.: Transcendental Numbers and Diophantine Approximations. Bull. AMS 77/5, 635–677 (1971).MATHCrossRefGoogle Scholar
  69. [69]
    Lankford, D. S.: Canonical Algebraic Simplification. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-25, 1975.Google Scholar
  70. [70]
    Lankford, D. S.: Canonical Inference. Univ. of Texas, Austin: Dept. Math. Comput. Sci., Rep. ATP-32, 1975.Google Scholar
  71. [71]
    Lankford, D. S.: Research in Applied Equational Logic. Louisiana Tech. Univ., Ruston: Math. Dept., MTP-15, 1980.Google Scholar
  72. [72]
    Lankford, D. S.: A Simple Explanation of Induetionless Induction. Louisiana Tech. Univ., Ruston: Math. Dept., MTP-14, 1981.Google Scholar
  73. [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
  74. [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
  75. [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
  76. [76]
    Lauer, M.: Canonical Representatives for Residue Classes of a Polynomial Ideal. SYMSAC 1976, 339–345.CrossRefGoogle Scholar
  77. [77]
    Lausch, H., Nöbauer, W.: Algebra of Polynomials. Amsterdam: North-Holland 1973.MATHGoogle Scholar
  78. [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
  79. Loos, R.: Toward a Formal Implementation of Computer Algebra. EUROSAM 1974, 9–16.Google Scholar
  80. [80]
    Loos, R.: Algorithmen und Datenstrukturen I: Abstrakte Datentypen. Univ. Karlsruhe, Federal Republic of Germany: Lecture Notes, 1980.Google Scholar
  81. [81]
    Loos, R.: Term Reduction Systems and Algebraic Algorithms. Proc. 5th Gl Workshop on Artif. Intell., Bad Honnef 1981, Informatik Fachberichte 47, 214–234 (1981).Google Scholar
  82. [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.Google Scholar
  83. [83]
    Luckham, D. C., German, S. M., Henke, F. W., Karp, R. A., Milne, P. W., Oppen, D. C., Polak, W., Scheriis, W. L.: Stanford PASCAL Verifier User Manual. Stanford Univ.: Comput. Sci. Dept., Rep. STAN-CS-79-731, 1979.Google Scholar
  84. [84]
    Manin, Y. I.: A Course in Mathematical Logic. Berlin-Heidelberg-New York: Springer 1977.MATHGoogle Scholar
  85. Manna, Z., Ness, S.: On the Termination of Markov Algorithms. Third Hawaii International Conference on System Sciences 1970, 789–792.Google Scholar
  86. [86]
    Martelli, A., Montanari, U.: An Effieient Unification Algorithm. Unpublished Report (1979).Google Scholar
  87. Martin, W. A.: Computer Input/Output of Mathematical Expressions. SYMSAM 1971, 78–89.Google Scholar
  88. [88]
    Martin, W. A.: Determining the Equivalence of Algebraic Expressions by Hash Coding. SYMSAM 1971, 305–310.Google Scholar
  89. [89]
    Matiyasevic, J.: Diophantine Representation of Recursively Enumerable Predicates. Proc. Second Scandinavian Logic Symp. Amsterdam: North-Holland 1970.Google Scholar
  90. [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
  91. [91]
    McDonald, I. D.: A Computer Application to Finitep-Groups. J. Aust. Math. Soc. 17, 102–112 (1974).CrossRefGoogle Scholar
  92. [92]
    Möller, H. M.: Mehrdimensionale Hermite-Interpolation und numerische Integration. Math. Z. 148, 107–118 (1976).MATHMathSciNetCrossRefGoogle Scholar
  93. [93]
    Moses, J.: Symbolic Integration. Ph.D. Thesis* Cambridge, Mass., M.I.T., Math. Dept., Rep. MAC-47, 1967.Google Scholar
  94. Moses, J.: Algebraic Simplification: A Guide for the Perplexed. SYMSAM 1971, 282–304 and Commun. ACM 14, 527–537 (1971).Google Scholar
  95. [95]
    Musser, D. R.: Algorithms for Polynomial Factorization. Univ. of Wisconsin, Madison: Ph.D. Thesis, Techn. Rep. 134, 1971.Google Scholar
  96. [96]
    Musser, D. R.: A Data Type Verification System Based on Rewrite Rules. USC Information Science Institute, Marina del Rey, Calif.: 1977.Google Scholar
  97. [97]
    Musser, D. R.: Convergent Sets of Rewrite Rules for Abstract Data Types. Information Sciences Institute: Report 1978.Google Scholar
  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
  99. [99]
    Newman, M. F.: Calculating Presentations for Certain Kinds of Quotient Groups. SYMSAC 1976, 2–8.CrossRefGoogle Scholar
  100. [100]
    Newman, M. H. A.: On Theories with a Combinatorial Definition of “Equivalence”. Ann. Math. 43/2, 223–243 (1942).MATHCrossRefGoogle Scholar
  101. [101]
    O’Donnell, M.: Computing in Systems Described by Equations. Lecture Notes in Computer Science, Vol. 58. Berlin-Heidelberg-New York,: Springer 1977.MATHGoogle Scholar
  102. [102]
    Oldehoeft, A.: Analysis of Constructed Mathematical Responses by Numeric Tests for Equivalence. Proc. ACM 24th Nat. Conf., 117–124 (1969).Google Scholar
  103. [103]
    Paterson, M. S., Wegmann, M. N.: Linear Unification. J. Comput. Syst. Sci. 16, 158–167 (1978).MATHCrossRefGoogle Scholar
  104. [104]
    Pavelle, R., Rothstein, M., Fitch, J.: Computer Algebra. Preprint, Scientific American 1981.Google Scholar
  105. [105]
    Peterson, G. E., Stickel, M. E.: Complete Set of Reductions for Some Equational Theories. J. ACM 28/2, 233–264 (1981).MATHMathSciNetCrossRefGoogle Scholar
  106. [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
  107. [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
  108. [108]
    Plotkin, G.: Building-In Equational Theories. Machine-Intelligence 7, 73–90 (1972).MATHMathSciNetGoogle Scholar
  109. [109]
    Pohst, M., Yun, D. Y. Y.: On Solving Systems of Algebraic Equations Via Ideal Bases and Elimination Theory. SYMSAC 1981, 206–21LCrossRefGoogle Scholar
  110. [110]
    Polak, W.: Program Verification at Stanford: Past, Present, Future. Stanford University: Comput. Syst. Lab., Rep. 1981.Google Scholar
  111. [111]
    Raulefs, P., Siekmann, J., Szabo, 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
  112. [112]
    Reynolds, J. C.: Reasoning About Arrays. Commun. ACM 22/5, 290–299 (1979).MATHMathSciNetCrossRefGoogle Scholar
  113. [113]
    Richardson, D.: Some Unsolvable Problems Involving Elementary Functions of a Real Variable. J. Symb. Logic 33, 511–520 (1968).CrossRefGoogle Scholar
  114. Richardson, D.: Solution of the Identity Problem for Integral Exponential Functions. Math. Logik Grundlagen Math. 15, 333–340 (1969)MATHMathSciNetCrossRefGoogle Scholar
  115. [115]
    Richter, M. M., Kemmenich, S.: Reduktionssysteme und Entscheidungsverfahren. Rhein.- Westf. Tech. Hochschule, Aachen: Inst. f. Informatik, Rep. 4, 1980.Google Scholar
  116. [116]
    Risch, R. H.: The Problem of Integration in Finite Terms. Trans. AMS 139, 167–189 (1969).MATHMathSciNetCrossRefGoogle Scholar
  117. [117]
    Robinson, J. A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12, 23–41 (1965).MATHCrossRefGoogle Scholar
  118. [118]
    Robinson, J. A.: Computational Logic: The Unification Computation. Machine Intelligence 6, 63–72. New York: Edinb. Univ. Press 1971.Google Scholar
  119. [119]
    Rogers, H.: Theory of Recursive Functions and Effective Computability. New York: McGraw- Hill 1967.MATHGoogle Scholar
  120. [120]
    Rosen, B. K.: Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM 20/1, 160–187 (1973).MATHCrossRefGoogle Scholar
  121. [121]
    Schaller, S.: Algorithmic Aspects of Polynomial iResidue Class Rings. Ph.D. Thesis, Comput. Sci. Tech., University of Wisconsin, Madison, Rep. 370, 1979.Google Scholar
  122. [122]
    Schräder, R.: Zur konstruktiven Idealtheorie. Dipl. Thesis, Math. Inst., Univ. of Karlsruhe, Federal Republic of Germany 1976.Google Scholar
  123. [123]
    Seidenberg, A.: Constructions in Algebra. Trans. AMS 197, 273–313 (1974).MATHMathSciNetCrossRefGoogle Scholar
  124. [124]
    Sethi, R.: Testing for the Church-Rosser Property. J. ACM 21/4, 671–679 (1974), 22/3, 424 (1975).MATHMathSciNetCrossRefGoogle Scholar
  125. [125]
    Shtokhamer, R.: Simple Ideal Theory: Some Applications to Algebraic Simplification. Univ. of Utah, Salt Lake City: Tech. Rep. UCP-36, 1975.Google Scholar
  126. [126]
    Shtokhamer, R.: A Canonical Form of Polynomials in the Presence of Side Relations. Technion, Haifa: Phys. Dept., Rep. 25, 1976.Google Scholar
  127. [127]
    Shtokhamer, R.: Attempts in Local Simplification of Non-Nested Radicals. SIGSAM Bull. 11/1, 20–21 (1977).CrossRefGoogle Scholar
  128. [128]
    Spear, D.: A Constructive Approach to Commutative Ring Theory. MACSYMA 1977, 369–376.Google Scholar
  129. [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
  130. [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
  131. [131]
    Stoutemyer, D. R.: Qualitative Analysis of Mathematical Expressions Using Computer Symbolic Mathematics. SYMSAC 1976, 97–104.CrossRefGoogle Scholar
  132. [132]
    Stoutemyer, D. R.: Automatic Simplification for the Absolute Value Function and its Relatives. ACM SIGSAM Bull. 10/4, 48–49 (1976).CrossRefGoogle Scholar
  133. [133]
    Suzuki, N., Jefferson, D.: Verification Decidability of Presburger Array Programs. J. ACM 27/1, 191–205 (1980).MATHMathSciNetCrossRefGoogle Scholar
  134. [134]
    Szekeres, G.: A Canonical Basis for the Ideals of a Polynomial Domain. Am. Math. Mon. 59/6, 379–386 (1952).MATHMathSciNetCrossRefGoogle Scholar
  135. [135]
    Tobey, R. G.: Experience with FORMAC Algorithm Design. Commun. ACM 9, 589–597 (1966).MATHCrossRefGoogle Scholar
  136. [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
  137. [137]
    Trinks, W.: Über B. Buchbergers Verfahren, Systeme algebraischer Gleichungen zu lösen. J. Number Theory 10/4, 475–488 (1978).MATHMathSciNetCrossRefGoogle Scholar
  138. [138]
    Trotter, P. G.: Ideals in Z[x,y]. Acta Math. Acad. Sci. Hungar. 32 (1–2), 63–73 (1978).MATHMathSciNetCrossRefGoogle Scholar
  139. Winkler, F., Buchberger, B., Lichtenberger, F., Rolletschek, H.: An Algorithm for Constructing Canonical Bases (Gröbner-Bases) for Polynomial Ideals. (Submitted.)Google Scholar
  140. [140]
    Yun, D. Y. Y., Stoutemyer, R. D.: Symbolic Mathematical Computation. Encyclopedia of Computer Science and Technology (Beizer, J., Holzman, A. G., Kent, A., eds.), Vol. 15, pp. 235–310. New York-Basel: Marcel Dekker 1980.Google Scholar
  141. [141]
    Zacharias, G.: Generalized Gröbner Bases in Commutative Polynomial Rings. Bachelor Thesis, Dept. Comput. Sci., M.I.T., 1978.Google Scholar
  142. [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 1983

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 Karlsruhe Zirkel 2KarlsruheFederal Republic of Germany

Personalised recommendations