Skip to main content
SpringerLink
Log in

Basic features and development of the critical-pair/completion procedure

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1985)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 202))

Included in the following conference series:

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Aho, A., Sethi, R., and Ullman, J.D., 1972: Code Optimization and finite Church-Rosser theorems. In: Design and Optimisation of Compilers (ed. by R. Rustin), Prentice Hall, 89–105.

    Google Scholar 

  • Armbruster, D., 1985: Bifurcation theory and computer algebra: an initial approach. Proc. EUROCAL 85, LNCS, Springer,to appear.

    Google Scholar 

  • Bachmair, L., and Buchberger, B., 1980: A simplified proof of the characterization theorem for Gröbner bases. ACM SIGSAM Bull 14/4, 29–34.

    Google Scholar 

  • Bachmair, L., and Plaisted, D.A., 1985: Termination orderings for associative commutative rewriting systems. J. of Symbolic Computation (Academic Press), to appear.

    Google Scholar 

  • Ballantyne, A.M., and Lankford, D.S., 1981: New decision algorithms for finitely presented commutative semigroups. Computers and Maths. with Appls. 7, 159–165; preliminary version: Rep. MTP-4, Louisiana Tech Univ., Dep. of Math. 1979.

    Google Scholar 

  • Ballantyne, M., Butler, G., and Lankford, D., 1984: On practical uniform decision algorithms for the uniform word problem in finitely presented commutative rings of characteristics ∞, ..., 3, 2, 1. Tech. Report, Louisiana Tech Univ., Dep. of Math.

    Google Scholar 

  • Bauer, G., 1981: The representation of monoids by confluent rule systems. Ph.D. thesis, University of Kaiserlautern (FRG), Dept. of Comp. Scie.

    Google Scholar 

  • Bauer, G., and Otto, F, 1984: Finite complete rewriting systems and the complexity of the word problem. Manuscript, Univ. of Kaiserslautern, Dep. Comp. Scie.

    Google Scholar 

  • Bayer, D., 1982: The division algorithm and the Hilbert scheme. Ph.D. thesis, Harvard University, Cambridge, Mass., Math. Dept.

    Google Scholar 

  • Bergman, G.M., 1978: The diamond lemma for ring theory. Advances in Math. 29, 178–218.

    Google Scholar 

  • Blass, A., and Gurevich, Yu., 1983: Equivalence relations, invariants, and normal forms. Proc. Logic and Machines: Decision Problems and Complexity, (ed. by E. Börger, G. Hasenjaeger, D.Rödding), Springer LNCS 171, 24–42.

    Google Scholar 

  • Böge, W., Gebauer, R., and Kredl, H., 1985: Gröbner-Bases using SAC2. Proc. EUROCAL 85, to appear.

    Google Scholar 

  • Book, R.V., 1982: Confluent and other types of Thue systems. J. ACM 29/1, 171–182.

    Google Scholar 

  • Book, R.V., 1982a: The power of the Church-Rosser property for string rewriting systems. Proc. 6th Conference on Automated Deduction, New York, (ed. by D. W. Loveland), Springer LNCS 138, 360–368.

    Google Scholar 

  • Book, R.V., 1985: Thue systems as rewriting systems. These proceedings.

    Google Scholar 

  • Brandt, D., Darringer, J.A., and Joyner, W.H., 1978: Completeness of conditional reductions. IBM Research Center, Yorktown Heights.

    Google Scholar 

  • Buchberger, B., 1965: An algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal (German). Ph.D. thesis, Univ. of Innsbruck (Austria), Math. Inst.

    Google Scholar 

  • Buchberger, B., 1970: An algorithmical criterion for the solvability of algebraic systems of equations (German). Aequationes mathematicae, 4/3, 374–383.

    Google Scholar 

  • Buchberger, B., 1976: A theoretical basis for the reduction of polynomials to canonical form. ACM SIGSAM Bull. 10/3, 19–29 and 10/4, 19–24.

    Google Scholar 

  • Buchberger, B., 1979: A criterion for detecting unnecessary reductions in the construction of Gröbner bases. Proc. EUROSAM 79, Marseille, June 1979, (ed. by W. Ng), Springer LNCS 72, 3–21.

    Google Scholar 

  • Buchberger, B., 1982: Miscellaneous Results on Gröbner bases for polynomial ideals II. Techn. Report CAMP 82-23, Univ. of Linz, Math. Inst.; also Techn. Report 83-1, Univ. of Delaware, Dep. of Comp. and Inform. Scie.

    Google Scholar 

  • Buchberger, B., 1983: A note on the complexity of constructing Gröbner bases. Proc. EUROCAL 83, London, March 1983, (ed. by J. A. van Hulzen), Springer LNCS 162, 137–145.

    Google Scholar 

  • Buchberger, B., 1983a: A critical-pair/completion algorithm for finitely generated ideals in rings. Proc. Logic and Machines: Decision Problems and Complexity, (ed. by E. Börger, G. Hasenjaeger, D.Rödding), Springer LNCS 171, 137–161.

    Google Scholar 

  • Buchberger, B., 1983b: Gröbner bases: an algorithmic method in polynomial ideal theory. Techn. Report CAMP-83.29, Univ. of Linz, Math. Inst.; to appear as Chapter 6 in: Recent Trends in Multidimensional Systems Theory (ed. by. N. K. Bose), Reidel, 1985.

    Google Scholar 

  • Buchberger, B., 1984: Mathematics for computer science II — algorithm types and problem solving strategies. Lecture notes, Univ. of Linz, Math. Institute, CAMP-Nr. 84-4.0.

    Google Scholar 

  • Buchberger, B., and Loos, R., 1982: Algebraic simplification. In: Computer Algebra — Symbolic and Algebraic Computation (ed. by B. Buchberger, G. Collins, R. Loos eds.), Springer, Wien — New York, 11–43.

    Google Scholar 

  • Bücken, H., 1979: Reduction systems and word problems (German). Rep. 3, RWTH, Aachen, FRG, Computer Science Inst.

    Google Scholar 

  • Bücken, H., 1979: Reduction systems and small cancellation theory. Proc. 4th Workshop on Automated Deduction, 53–59.

    Google Scholar 

  • Butler, G., Lankford, D., 1980: Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras. Techn. Rep. MTP-7, Louisiana Tech. Univ., Dep. of Math.

    Google Scholar 

  • Butler, G., Lankford, D., 1984: Dickson's lemma, Hilbert's basis theorem, and applications to completion in commutative noetherian rings. Manuscript, Dept. Math. and Statistics, Louisiana Tech. Univ., Ruston.

    Google Scholar 

  • Cardoza, E., Lipton, R., and Meyer, A.R., 1976: Exponential space complete problems for Petri nets and commutative semigroups. Conf. Record of the 8th Annual ACM Symp. on Theory of Computing, 50–54.

    Google Scholar 

  • Castro, F., 1984: Theoreme de division pour les opérateurs differentiels et calcul des multiplicités. These 3eme cycle, Univ. Paris VII.

    Google Scholar 

  • Chang, C., and Lee, R.C., 1973: Symbolic logic and mechanical theorem proving. Academic Press.

    Google Scholar 

  • Church, A., Rosser, J.B., 1936: Some properties of conversion. Trans. AMS 39, 472–482.

    Google Scholar 

  • Collins, G., 1975: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. Proc. 2nd GI Conf. on Automata Theory and Formal Languages, (ed. by H. Brakhage), Kaiserslautern, Springer LNCS 33, 134–183.

    Google Scholar 

  • Collins, G.E., and Loos, R.G., 1980: ALDES and SAC-2 now available. ACM SIGSAM Bulletin Vol. 14/2, p. 19.

    Google Scholar 

  • Coquand, T., and Huet, G., 1985: Constructions: a higher order proof system for mechanizing mathematics. Invited paper in Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Cousineau, G., 1984: Preuves de terminaison des systemes de reecriture. Notes de cours de DEA, University Paris 7.

    Google Scholar 

  • Davis, M. (ed.), 1965: The undecidable: basic papers on undecidable propositions, unvsolvable problems and computable functions. Raven Press, Hewlett, New York.

    Google Scholar 

  • Dehn, M., 1911: On infinte discontinuous groups (German). Math. Ann. 71, 116–144.

    Google Scholar 

  • Dershowitz, N., 1979a: Orderings for term-rewriting systems. Proc. 20th Symp. on Foundations of Comp. Sci., 123–131.

    Google Scholar 

  • Dershowitz, N., 1979b: A note on simplification orderings. Inf. Process. Lett. 9/5, 212–215.

    Google Scholar 

  • Dershowitz, N., 1982: Orderings for term-rewriting systems. J. of Theoretical Computer Science 17, 279–301.

    Google Scholar 

  • Dershowitz, N., 1982a: Applications of the Knuth-Bendix completion procedure. Prelim. rep., Univ. of Illinois at Urbana-Champaign, Dep. Comp. Scie.

    Google Scholar 

  • Dershowitz, N., 1985: Termination issues in term rewriting systems. These proceedings.

    Google Scholar 

  • Dershowitz, N., and Manna, Z., 1979: Proving termination with multiset orderings. Comm. ACM 22, 465–475.

    Google Scholar 

  • Dershowitz, N., Hsiang J., Josephson, N.A., and Plaisted, D.A., 1983: Associative-commutative rewriting. Proc. 10th IJCAI, Karlsruhe 1983, 990–994.

    Google Scholar 

  • Detlefs, D., Forgaard, R., 1985: A procedure for automatically proving the termination of a set of rewrite rules. These proceedings.

    Google Scholar 

  • Dick, A.J.J., 1985: ERIL — Equational reasoning: an interactive laboratory. Proc. EUROCAL 85, LNCS, Springer, to appear.

    Google Scholar 

  • Dickson, L.E., 1913: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. of Math. 35, 413–426.

    Google Scholar 

  • Evans, T., 1951: On multiplicative systems defined by generators and relations I; normal form theorems. Proc. Cambridge Philosophy Soc. 47, 637–649.

    Google Scholar 

  • Evans, T., 1951a: The word problem for abstract algebras. The J. of the London Math. Soc. 26, 64–71.

    Google Scholar 

  • Evans, T., 1978: Word problems. Bull. AMS 84/5, 789–802.

    Google Scholar 

  • Fages, F., 1983: Formes canoniques dans les algèbres booléennes et applications à la démonstration automatique en logique de premier ordre. These 3eme cycle, Universite Paris VI.

    Google Scholar 

  • Fages, F., 1984: Associative-commutative unification. Proc. 7th CADE, (ed. by R. Shostak), Napa Valley, Springer LNCS 170.

    Google Scholar 

  • Fages, F., 1985: KB reference manual. INRIA Rep. no. 368.

    Google Scholar 

  • Fages, F., and Huet, G., 1983: Complete sets of unifiers and matchers in equational theories. Proc. CAAP 83, L' Aqila, (ed. by G. Ausiello, M.Protasi), Springer LNCS 159, 205–220.

    Google Scholar 

  • Fay, M., 1979: First order unification in equational theories. Proc. 4th CADE, Springer LNCS 87, 161–167.

    Google Scholar 

  • Forgaard, R., and Guttag, J.V., 1984: REVE: A term rewriting system generator with failure-resistent Knuth-Bendix. MIT-LCS.

    Google Scholar 

  • Fortenbacher, A., 1985: An algebraic approach to unification under associativity and commutativity. These proceedings.

    Google Scholar 

  • Futatsugi, K., Goguen, J., Jouannaud, J.P., Mesenguer, J., 1985: Principles of OBJ2. Proc. of the 1985 Symp. on Principles of Progr. Lang., to appear.

    Google Scholar 

  • Galligo, A., 1979: The division theorem and stability in local analytic geometry (French). Extrait des Annales de l'Institut Fourier, Univ. of Grenoble, 29/2.

    Google Scholar 

  • Galligo, A., 1984: Algorithmes de calcul de base standards. Manuscript, Univ. of Nice, France.

    Google Scholar 

  • Galligo, A., 1985: Some algorithmic questions on ideals of differential operators. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • 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., 1980: An overview on AFFIRM: a specification and verification system. In: Information Processing 80 (ed. by S.H. Lavington), North-Holland, 343–387.

    Google Scholar 

  • Gianni, P., and Trager, B., 1985: GCD's and factoring multivariate polynomials using Gröbner bases. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Giusti, M., 1984: Some effectivity problems in polynomial ideal theory. Proc. EUROSAM 84, Cambridge, (ed. J. Fitch), Springer LNCS 174, 159–172.

    Google Scholar 

  • Giusti, M., 1985: A note on the complexity of constructing standard bases. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Goad, C.A., 1980: Proofs of descriptions of computation. Proc. 5th CADE, Springer LNCS 87, 39–52.

    Google Scholar 

  • Göbel, R., 1983: A completion procedure for globally finite term rewriting systems. Proc. of an NSF Workshop on the Rewrite Rule Laboratory, General Electric, 1983, Schenectady, (ed. by J.V. Guttag, D. Kapur, D.R. Musser), Rep. no. 84 GEN008, 155–206.

    Google Scholar 

  • Goguen, J.A., 1980: How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementations. Proc. 5th CADE, (ed. by W.Bibel and R. Kowalski), Springer LNCS 87, 356–373. 222

    Google Scholar 

  • Goguen, J.A., Meseguer, J., and Plaisted, D., 1982: Programming with parameterized abstract objects in OBJ. In: Theory and Practice of Software Technology (ed. by D. Ferrari, M. Bolognani and J. Goguen), North-Holland, 163–193.

    Google Scholar 

  • Greenlinger, M., 1960: Dehn's algorithm for the word problem. Comm. on Pure and Applied Math. 13. 67–83.

    Google Scholar 

  • Gröbner, W., 1950: On elimination theory (German). Monatshefte für Mathematik 54, 71–78.

    Google Scholar 

  • Guiver, J.P., 1982: Contributions to two-dimensional systems theory. Ph. D. thesis, Univ. of Pittsburgh, Math. Dept.

    Google Scholar 

  • Guttag, J.V., Kapur D., and Musser, D.R., (eds.), 1984: Proc. of an NSF Workshop on the Rewrite Rule Laboratory, Sept. 6–9, 1983, General Electric, Schenectady, NY, Rep. no. 84GEN008.

    Google Scholar 

  • Hearn, A.C., 1984: Reduce user's manual: version 3.1. The Rand Corporation, Santa Monica, California.

    Google Scholar 

  • Herbrand, J., 1930: Researches in the theory of demonstration. Ph.D. thesis, Univ. of Paris; reprinted in: From Frege to Gödel: A Source Book in Mathematical Logic, (ed. by van J. Heijenoort), Harvard Univ. Press, Cambridge, Mass.

    Google Scholar 

  • Hermann, G., 1926: The question of finitely many steps in the theory of polynomial ideals (German). Math. Ann. 95, 736–788.

    Google Scholar 

  • Hindley, R., 1969: An abstract form of the Church-Rosser theorem I. J. of Symbolic Logic, 34/4, 545–560.

    Google Scholar 

  • Hindley, R., 1974: An abstract form of the Church-Rosser theorem II: applications. J. of Symbolic Logic 39+1, 1–21.

    Google Scholar 

  • Hironaka, H., 1964: Resolution of singularities of an algebraic variety over a field of characteristic zero: I, II. Annals of Math., 79, 109–326.

    Google Scholar 

  • Hsiang, J., 1981: Refutational theorem proving using term rewriting systems. AI J. 1985. Manuscript, Univ. of Illinois at Urbana Champaign, Dep. Comp. Scie.

    Google Scholar 

  • Hsiang, J., 1982: Topics in automated theorem proving and program generation. AI J. 1985. Ph. d. thesis, Univ. of Illinois at Urbana-Champaign, Dept. of Comp. Scie.

    Google Scholar 

  • Hsiang, J., 1985: Two results in term rewriting theorem proving. These proceedings.

    Google Scholar 

  • Hsiang, J., and Dershowitz, N., 1983: Rewrite methods for clausal and non-clausal theorem proving. Proc. ICALP 83, 10th Colloqium, Barcelona, Spain, Springer LNCS 154, 331–346.

    Google Scholar 

  • Hsiang, J., and Plaisted, D., 1982: Deductive program generation. Techn. Rep., Univ. of Illinois at Urbana-Champaign, Comp. Scie. Dept.

    Google Scholar 

  • Huet, G., 1976: Résolution d'équation dans des languages d'ordre 1, 2, ..., ω. Thèse d'etat, Univ. Paris VII.

    Google Scholar 

  • Huet, G., 1977: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27 (1980), 797–821; preprint: 21st FOCS.

    Google Scholar 

  • Huet, G., 1978: An algorithm to generate the basis of solutions to homogenous linear diophantine equations. Information Processing Letters 7/3, 144–147.

    Google Scholar 

  • Huet, G., 1981: A complete proof of the Knuth-Bendix completion algorithm. J. Comp. and System Sci. 23, 11–21.

    Google Scholar 

  • Huet, G., and Hullot, J.M., 1980: Proofs by induction in equational theories with constructors. 21st IEEE Symp. on Foundations of Comp. Scie., 96–107; also: J. ACM 25 (1982), 239–266.

    Google Scholar 

  • Huet, G., and Lankford, D.S., 1978: On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA, Rocquencourt, Les Chesnay, France.

    Google Scholar 

  • Huet, G., and Oppen, D.C., 1980: Equations and rewrite rules: a survey. In: Formal Language Theory, Perspectives and Open Problems (ed. by R. V. Book), Academic Press, 349–405.

    Google Scholar 

  • Hullot, J.M., 1979: Associative-commutative pattern matching. 5th IJCAI, Tokyo.

    Google Scholar 

  • Hullot, J.M., 1980: A catalogue of canonical term rewriting systems. Techn. Rep. CSL-113, SRI International, Menlo Park, Calif.

    Google Scholar 

  • Hullot, J.M., 1980a: Canonical forms and unification. Proc. 5th CADE, (ed. by W. Bibel and R. Kowalski), Springer LNCS 87, 318–334.

    Google Scholar 

  • Hullot, J.M., 1980 a: Compilation de formes canoniques dans les theories équationnelles. Thèse 3ème cycle, U. Paris Sud.

    Google Scholar 

  • Hussmann, H., 1985: Unification in conditional equational theories. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Huynh, D.T., 1984: The complexity of the membership problem for two subclasses of polynomial ideals. Manuscript, Iowa State Univ., Ames, Comp. Scie. Dep.

    Google Scholar 

  • Jeanrond, J., 1980: Deciding unique termination of permutative rewrite systems: choose your term algebra carefully. Proc. 5th CADE, (ed. by W. Bibel and R. Kowalski), Springer LNCS 87.

    Google Scholar 

  • Jenks, R.D., 1984: A primer: 11 keys to NEW SCRATCHPAD. Proc. EUROSAM 84, Cambridge, England, (ed. by J. Fitch), Springer LNCS 174, 123–147.

    Google Scholar 

  • Jouannaud, J.P., 1983: Confluent and coherent equational term rewriting systems. Proc. CAAP 83, L' Aqila, (ed. by G. Ausiello, M.Protasi), Springer LNCS 159, 269–283.

    Google Scholar 

  • Jouannaud, J.P., and Kirchner, H., 1984: Completion of a set of rules modulo a set of equations. Techn. Rep. SRI International, Menlo Park, Calif.; see also: Proc. of an NSF Workshop on the Rewrite Rule Raboratory, General Electric, 1983, Schenectady, (ed. by J.V. Guttag, D. Kapur, D.R. Musser), Rep. no. 84GEN008, pp.207–228.

    Google Scholar 

  • Jouannaud, J.P., Kirchner, C., and Kirchner, H., 1983: Incremental construction of unification algorithms in equational theories. Proc. ICALP 83, 10th Colloqium, Barcelona, Spain, Springer LNCS 154, 361–373.

    Google Scholar 

  • Jouannaud, J.P., Kirchner H., and Remy, J.L., 1983: Church-Rosser properties of weakly terminating equational term rewriting systems. Proc. 10th IJCAI, Karlsruhe.

    Google Scholar 

  • Jouannaud, J.P., Lescanne, P., and Reinig, F., 1982: Recursive decomposition ordering. Conf. on Formal Description of Programming Concepts, (D. Bjorner), North Holland.

    Google Scholar 

  • Jouannaud, J.P., and Lescanne, P., 1982: On multiset orderings. Information Processing Letters 15, 57–62.

    Google Scholar 

  • Jouannaud, J.P., and Munoz, M., 1984: Termination of a set of rules modulo a set of equations. Proc. 7th CADE, (ed. by R. Shostak), Springer LNCS 170, 175–193.

    Google Scholar 

  • Kamin, Lévy, 1980: Attempts for generalizing the recursive path ordering. Unpublished manuscript, Univ. of Paris 7.

    Google Scholar 

  • Kandri-Rody, A., 1984: Effective methods in the theory of polynomial ideals. Ph.D. thesis, Rensselaer Polytechnic Institute, Troy, NY, Math. Dep.

    Google Scholar 

  • Kandri-Rody, A., and Kapur, D., 1983: On relationship between Buchberger's Gröbner basis algorithm and the Knuth-Bendix completion procedure. Rep. no. 83CRD286, General Electric, Schenectady.

    Google Scholar 

  • Kandri-Rody, A., and Kapur, D., 1984: Computing the Gröbner basis of an ideal in polynomial rings over the integers. 3rd MACSYMA Userss' Conf., Schenectady, NY, July 1984.

    Google Scholar 

  • Kandri-Rody, A., and Kapur, D., 1984a: Algorithms for computing Gröbner bases of polynomial ideals over various Euclidean rings. Proc. EUROSAM 84, Cambridge, (ed. J. Fitch), Springer LNCS vol. 174, 195–206.

    Google Scholar 

  • Kandri-Rody, A., Kapur, D., Narendran, P., 1985: An ideal-theoretic approach to word problems and unification problems over finitely presented commutative algebras. These proceedings.

    Google Scholar 

  • Kanger, S., 1957. Provability in logic. Stockholm.

    Google Scholar 

  • Kaplan, S., 1984: Fair conditional rewriting systems: unification, termination and confluence. Techn. Rep. No. 194, Lab. de Recherche en Informatique, Orsay, France.

    Google Scholar 

  • Kapur, D., and Krishnamurthy, B., 1983: A natural proof system based on rewriting techniques. Proc. of an NSF Workshop on the Rewrite Rule Laboratory, General Electric, Schenectady, 1983, (ed. by J.V. Guttag, D. Kapur, D.R. Musser), Rep. no. 84GEN008, 337–348.

    Google Scholar 

  • Kapur, D., and Narendran, P., 1985: An equational approach to theorem proving in first-order predicate calculus. Proc. IJCAI 1985, Los Angeles, to appear.

    Google Scholar 

  • Kapur, D., and Sivakumar, G., 1983: Architecture of and experiments with RRL, a rewrite rule laboratory. Proc. of an NSF Workshop on the Rewrite Rule Laboratory, General Electric, Schenectady, (ed. by J. V. Guttag, D. Kapur, D. R. Musser), Rep. no. 84GEN008, 33–56.

    Google Scholar 

  • Kirchner, C., 1984: A new equational unification method: a generalization of Martelli-Montanari algorithm. Proc. 7th CADE, (ed. by R. Shostak), Springer LNCS 170.

    Google Scholar 

  • Kirchner, C., and Kirchner, H., 1983: Current implementation of the general E-completion algorithm. Techn. Rep., Centre de Recherches en Informatique de Nancy.

    Google Scholar 

  • Kirchner, H., 1984: A general inductive completion algorithm and application to abstract data types. Proc. 7th CADE, (ed. by R. Shostak), Springer LNCS 170.

    Google Scholar 

  • Kirchner, C., and Kirchner, H., 1985: Implementation of a general completion procedure parameterized by built-in theories and strategies. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Knuth, D.E., 1970: Notes on central groupoids. J. Comb. Theory 8, 376–390.

    Google Scholar 

  • Knuth, D.E., and Bendix, P. B., 1967: Simple word problems in universal algebras. Proc. of the Conf. on Computational Problems in Abstract Algebra, Oxford, 1967, (ed. by J. Leech), Pergamon Press, Oxford, 1970, 263–298.

    Google Scholar 

  • Kollreider, C., 1978: Polynomial reduction: the influence of the ordering of terms on a reduction algorithm. Techn. Rep. CAMP 78-4, Univ. of Linz, Austria (Europe), Math. Dep.

    Google Scholar 

  • Kruskal, J.B., 1960: Well-quasi-ordering, the tree theorem and Vazsonyi's conjecture. Trans. AMS 95, 210–225.

    Google Scholar 

  • Küchlin, W., 1982: A theorem-proving approach to the Knuth-Bendix completion algorithm. Proc. EUROCAM 82, Marseille, (ed. by J. Calmet), Springer LNCS, 144, 101–108.

    Google Scholar 

  • Küchlin, W., 1982a: An implementation and investigation of the Knuth-Bendix completion procedure. Internal Rep., Comp. Scie. Dept., Univ. of Karlsruhe, FRG.

    Google Scholar 

  • Küchlin, W., 1985: A confluence criterion based on the generalized Newman lemma. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Kutzler, B., and Stifter, S., 1985: Geometrical theorem proving: a comparison between Wu's algorithm and the use of Gröbner bases. Tech. Rep. CAMP 85-17.0, Univ. of Linz, Math. Dept., to appear.

    Google Scholar 

  • Lankford, D.S., 1975: Canonical algebraic simplification. Rep. ATP-25, Univ. of Texas, Austin, Dep. Math. Comp. Sci.

    Google Scholar 

  • Lankford, D.S., 1975a: Canonocal inference. Rep. ATP-32, Univ. of Texas, Austin, Dep. Math. Comp. Sci.

    Google Scholar 

  • Lankford, D.S, 1979: A unification algorithm for abelian group theory. Rep. MTP-1, Louisiana Tech Univ., Math. Dep.

    Google Scholar 

  • Lankford, D.S., 1979a: Mechanical theorem proving in field theory. Rep. MTP-2, Louisiana Tech Univ., Math. Dep.

    Google Scholar 

  • Lankford, D.S., 1979b: On proving term rewriting systems are noetherian. Rep. MTP-3, Louisiana Tech Univ., Math. Dep.

    Google Scholar 

  • Lankford, D.S., 1979c: Some new approaches to the theory and applications of conditional term rewriting systems. Rep. MTP-6, Louisiana Tech Univ., Math. Dep.

    Google Scholar 

  • Lankford, D.S., 1980: Research in applied equational logic. Rep. MTP-15, Louisiana Tech Univ., Ruston, Math. Dep.

    Google Scholar 

  • Lankford, D.S., 1981: A simple explanation of inductionless induction. Rep. MTP-14, Louisiana Tech Univ., Ruston, Math. Dep.

    Google Scholar 

  • Lankford, D.S., and Ballantyne, A.M., 1977a: Decision procedures for simple equational theories with commutative axioms: Complete sets of commutative reductions. Rep. ATP-35, Univ. of Texas, Austin: Dep. Math. Comp. Sci.

    Google Scholar 

  • Lankford, D.S., and Ballantyne, A.M., 1977b: Decision procedures for simple equational theories with permutative axioms: Complete sets of permutative reductions. Rep. ATP-37, Univ. of Texas, Austin: Dep. Math. Compu. Sci.

    Google Scholar 

  • Lankford, D.S., and Ballantyne, A.M., 1977c: Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Rep. ATP-39, Univ. of Texas, Austin: Dep. Math. Comp. Sci.

    Google Scholar 

  • Lankford, D.S., and Ballantyne, A.M., 1979: The refutation completeness of blocked permutative narrowing and resolution. 4th CADE, Austin, 53–59.

    Google Scholar 

  • Lankford, D.S., and Butler, G., 1984: On the foundations of applied equational logic. Tech. Rep., Louisiana Tech Univ., Dep. of Math.

    Google Scholar 

  • Lankford, D.S., and Butler, G., 1984: On faster Smith normal form algorithms. Manuscript, Louisiana Tech Univ., Dep. of Math.

    Google Scholar 

  • Lankford, D.S, Butler, G., and Ballantyne, A.M., 1983: A progress report on new decision algorithms for finitely presented abelian groups. Proc. of an NSF Workshop on the Rewrite Rule Laboratory, General Electrics Schenectady, 1983, (ed. by J.V. Guttag, D. Kapur, D.R. Musser), Rep. no. 84 GENO08, 137–154.

    Google Scholar 

  • Lauer, M., 1976: Canonical representatives for residue classes of a polynomial ideal. Diploma thesis, Univ. of Kaiserslautern, Dep. Math.

    Google Scholar 

  • Lauer, M., 1976a: Canonical representatives for residue classes of a polyomial ideal. Proc. ACM SYMSAC 76, Yorktown Heights, N. Y., (ed. by R. D. Jenks), 339–345.

    Google Scholar 

  • Lazard, D., 1982: Commutative algebra and computer algebra. Proc. EUROCAM 82, Marseille, France, (ed. by J. Calmet), Springer LNCS 144, 40–48.

    Google Scholar 

  • Lazard, D., 1983: Gröbner bases, Gaussian elimination and resolution of systems of algebraic equations. Proc. EUROCAL 83, London, (ed. by J. A. van Hulzen), Springer LNCS 162, 146–156.

    Google Scholar 

  • Le Chenadec, P., 1983: Formes canoniques dans les algèbres finiment présentées. Thèse 3ème cycle, Univ. Paris-Sud, Centre d' Orsay. English version 1984.

    Google Scholar 

  • Le Cenadec, P., 1985: A Knuth-Bendix completion of some Coxeter groups. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Lescanne, P., 1981: Decomposition orderings as a tool to prove the termination of rewriting systems. Proc. 7th IJCAI, Vancouver, Canada, 548–550.

    Google Scholar 

  • Lescanne, P., 1983: Computer experiments with the REVE term rewriting system generator. Proc. 10th POPL conference, Austin, Texas.

    Google Scholar 

  • Lescanne, P., 1984: How to prove termination? An approach to the implementation of a new recursive decomposition ordering. Proc. 6th Conf. on Automata, Algebra and Programming, Bordeaux.

    Google Scholar 

  • Lichtenberger, F., 1980: PL/ADT: a system for using algebraically specified abstract data types (German). Ph.d. thesis, Univ. of Linz, Austria (Europe), Math. Inst.

    Google Scholar 

  • Lipton, R., and Snyder, L., 1977: On the halting problem of tree replacement systems. Conf. on Theoretical Computer Science, U. of Waterloo, 43–46.

    Google Scholar 

  • Livesey, M., and Siekmann, J., 1976: Unification of bags and sets. Techn. Report, Univ. of Karlsruhe, FRG, Comp. Sci. Dep.

    Google Scholar 

  • Llopis de Trias, R., 1983: Canonical forms for residue classes of polynomial ideals and term rewriting systems. Techn. Rep., Univ. Autónoma de Madrid, División de Matemática.

    Google Scholar 

  • Loos, R., 1981: Term reduction systems and algebraic algorithms. Proc. GWAI-81, Bad Honnef, (ed. by J. H. Siekmann), Springer Informatik-Fachberichte 47, 214–234.

    Google Scholar 

  • Loveland, D.W., 1978: Automated theorem proving: a logical basis. North-Holland, Amsterdam — New York — Oxford.

    Google Scholar 

  • MacDonald, I.D., 1974: A computer application to finite p-groups. J. Austral. Math. Soc. 17, 102–112.

    Google Scholar 

  • Makanin, G. S., 1977: The problem of solvability of equations in a free semigroup. Dokl. AN SSSR 233/2.

    Google Scholar 

  • Manna, Z., and Ness, S., 1970: On the termination of Markov algorithms. 3rd Hawai Internat. Conf. on System Scie., 789–792.

    Google Scholar 

  • Manna, Z., Waldinger, R., 1985: Special relations in automated deduction. Proc. of the 12th ICALP, Nafplion (Greece), Springer LNCS, to appear.

    Google Scholar 

  • Mayr, E. W., and Meyer, A. R., 1981: The complexity of the word problems for commutative semigroups and polynomial ideals. Report LCS/TM-199, M.I.T., Laboratory of Computer Science.

    Google Scholar 

  • Metivier, B., 1983: About the rewriting systems produced by the Knuth-Bendix completion algorithm. Information Processing Letters 16, 1983.

    Google Scholar 

  • Möller, H.M., 1976: Multidimensional Hermite-interpolation and numerical integration. Math. Z. 148, 107–118.

    Google Scholar 

  • Möller, H.M., 1985: A reduction strategy for the Taylor resolution. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Möller, H.M., and Buchberger, B., 1982: The construction of multivariate polynomials with preassigned zeros. Proc. EUROCAM 82, Marseille, (ed. by J. Calmet), Springer LNCS 144, 24–31.

    Google Scholar 

  • Möller, H.M., and Mora, F., 1984: Upper and lower bounds for the degree of Gröbner bases. Proc. EUROSAM 84, Cambridge, (ed. by J. Fitch), Springer LNCS, 174, 172–183.

    Google Scholar 

  • Mora, F., 1982: An algorithm to compute the equations of tangent cones. Proc. EUROCAM 82, Marseille, (ed. J. Calmet), Springer LNCS 144, 158–165.

    Google Scholar 

  • Mora, F., 1985: An algorithmic approach to local rings. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Mora, F., 1985a: Gröbner bases and standard bases for non-commutative polynomial rings. AAECC-3 conference, Grenoble, July 1985.

    Google Scholar 

  • Mora, F., and Möller, H. M., 1983: The computation of the Hilbert function. Proc. EUROCAL 83, London, (ed. by J. A. van Hulzen), Springer LNCS 162, 157–167.

    Google Scholar 

  • Mora, F., and Möller, H. M., 1983a: New constructive methods in classical ideal theory. Manuscript, Univ. of Genova, Italy, Math. Dept., submitted to publication.

    Google Scholar 

  • Muller, D.E., 1954: Application of Boolean algebra to switching circuit design & error detection. Trans. Inst. of Radio Eng., EC-3, 6–12.

    Google Scholar 

  • Munoz, M., 1983: Probleme de terminaison finie des systemes de reecriture equationels. Thèse 3ème cycle, Univ. Nancy 1.

    Google Scholar 

  • Musser, D.R., 1977: A data type verification system based on rewrite rules. Tech. Rep., USC Information Scie. Inst., Marina del Rey, Calif.

    Google Scholar 

  • Musser, D.R., 1978: Convergent sets of rewrite rules for abstract data types. Tech. Rep., USC Information Scie. Inst., Marina del Rey, Calif.

    Google Scholar 

  • Musser, D.R., 1978a: A data type verification system based on rewrite rules. 6th Texas Conf. on Computing Systems.

    Google Scholar 

  • Musser, D.R., 1980: On proving inductive properties of abstract data types. 7th ACM Symp. POPL, 154–162.

    Google Scholar 

  • Musser, D.R., 1980a: Abstract data type specification in the AFFIRM system. IEEE Trans. on S.E., Vol. SE-6, No.1.

    Google Scholar 

  • Musser, D.R., and Kapur, D., 1982: Rewrite rule theory and abstract data type analysis. Proc. EUROCAM 82, Marseille, France, (ed. by J. Calmet), Springer LNCS 144, 77–90.

    Google Scholar 

  • Nash-Williams, C.St.J.A., 1963: On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc. 59, 833–835.

    Google Scholar 

  • Newman, M.H.A., 1942: On theories with a combinatorial definition of "equivalence". Annals of Math., 43/2, 223–243.

    Google Scholar 

  • Padawitz, P., 1983: Equational data type specification and recursive program schema. IFIP Working Conf. on Formal Description of Programming Concepts II, (ed. by D. Bjorner), North-Holland.

    Google Scholar 

  • Paul, E., 1985: Equational methods in first order predicate calculus. J. of Symbolic Computation (Academic Press), Vol. 1/1, to appear.

    Google Scholar 

  • Paul, E., 1985a: On solving the equality problem in theories defined by Horn clauses. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Pavelle, R., and Wang, P.S., 1985: MACSYMA from F to G. J. of Symbolic Computation (Academic Press), Vol. 1/2, to appear.

    Google Scholar 

  • Pederson, J., 1984: Confluence methods and the word problem in universal algebra. Ph.D. thesis, Emory Univ., Dep. Math. and Comp. Scie.

    Google Scholar 

  • Pederson, J., 1985: Obtaining complete sets of reductions and equations without using special unification algorithms. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Perdrix, H., 1984: Propriétés Church-Rosser de systèmes de réécriture équationnels ayant la propriété de terminaison faible. Proc. STACS 84, Paris, (ed. M. Fontet, K. Mehlhorn), Springer LNCS 166, 97–108.

    Google Scholar 

  • Peterson, G.E., 1983: A technique for establishing completeness results in theorem proving with equality. SIAM J. of Computing 12/1, 82–100.

    Google Scholar 

  • Peterson, G.E., and Stickel, M.E., 1981: Complete sets of reductions for some equational theories. J. ACM 28/2, 233–264.

    Google Scholar 

  • Plaisted, D.A., 1978: Well-founded orderings for proving termination of systems of rewrite rules. Rep. 78–932, Univ. of Illinois at Urbana-Champaign, Dept. of Comp. Science.

    Google Scholar 

  • Plaisted, D.A., 1978a: A recursively defined ordering for proving termination of term rewriting systems. Rep. 78–943, Univ. of Illinois at Urbana-Champaign, Dept. of Comp. Science.

    Google Scholar 

  • Plaisted, D.A., 1983: An associative path ordering. Proc. of an NSF Workshop on the Rewrite Rule Laboratory, General Electrics, Schenectady, (ed. by J.V. Guttag, D. Kapur, and D.R. Musser), Rep. no. 84GEN008, 123–136.

    Google Scholar 

  • Plotkin, G., 1972: Building-in equational theories. Machine Intelligence 7, 73–90.

    Google Scholar 

  • Prawitz, D., 1960: An improved proof procedure. Theoria 26, 102–139.

    Google Scholar 

  • Raulefs, P., Siekmann, J., Szabó, P., Unvericht, E., 1979: A short survey on the state of the art in matching and unification problems. ACM SIGSAM Bull. 13/2, 14–20.

    Google Scholar 

  • Reed, I. S., 1954: A class of multiple error correcting codes and the decoding scheme. Trans. Inst. of Radio Eng., IT-4, 38–49.

    Google Scholar 

  • Remy, J.-L., 1982: Etude des systemes de recriture conditionnels et applications auy types abstraits algebriques. These d'etat, Nancy, France.

    Google Scholar 

  • Renschuch, B., 1976: Elementary and practical ideal theory (German). VEB Deutscher Verlag der Wissenschaften, Berlin.

    Google Scholar 

  • Rety, P., Kirchner, C., Kirchner, H., and Lescanne, P., 1985: Narrower, a new algorithm for unification and its application to logic programming. These proceedings.

    Google Scholar 

  • Richter, M.M., Kemmenich, S.: Reduction systems and decision procedures (German). Rep. 4, RWTH, Aachen, FRG, Comp. Sci. Inst.

    Google Scholar 

  • Robbiano, L., 1985: Term orderings on the polynomial ring. Proc. of the EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Robbiano, L., Valla, G., 1983: Some curves in P 3 are set-theoretic complete intersections. Manuscript, Univ. of Genova, Italy, Dep. Math.

    Google Scholar 

  • Robinson, G.A., and Wos, L.T., 1969: Paramodulation and theorem proving in first-order theories with equality. Machine Intelligence 4, American Elsevier, 135–150.

    Google Scholar 

  • Robinson, J.A., 1963: A machine-oriented logic (abstract). J. Symbolic Logic 28, 302.

    Google Scholar 

  • Robinson, J.A., 1965: A machine-oriented logic based on the resolution principle. J. ACM, 12/1, 23–41.

    Google Scholar 

  • Robinson, J.A., 1967: A review of automatic theorem proving. Proc. Symp. Appl. Math., Am. Math. Soc. 19, 1–18.

    Google Scholar 

  • Robinson, J.A., 1979: Logic: form and function. The mechanization of deductive reasoning. University Press, Edinburgh.

    Google Scholar 

  • Rosen, B.K., 1971: Subtree replacement systems. Ph.D. thesis, Harvard Univ.

    Google Scholar 

  • Rosen, B.K., 1973: Tree-manipulation systems and Church-Rosser theorems. J. ACM 20, 160–187.

    Google Scholar 

  • Rusinovitch, M., 1985: Plaisted ordering and recursive decomposition ordering revisited. These proceedings.

    Google Scholar 

  • Schaller, S., 1979: Algorithmic aspects of polynomial residue class rings. Ph.D. thesis, Techn. Rep. 370, Univ. of Wisconsin-Madison, Comp. Scie. Dept.

    Google Scholar 

  • Schrader, R., 1976: Contributions to constructive ideal theory (German). Diploma thesis, Univ. of Karlsruhe, FRG, Math. Inst.

    Google Scholar 

  • Sethi, R., 1974: Testing for the Church-Rosser property. J. ACM 21/4, 671–679.

    Google Scholar 

  • Shtokhamer, R., 1975: Simple ideal theory: some applications to algebraic simplification. Tech. Rep. UCP-36, Univ. of Utah, Salt Lake City.

    Google Scholar 

  • Shtokhamer, R., 1976: A canonical form of polynomials in the presence of side relations. Tech. Rep., Technion, Haifa, Phys. Dep.

    Google Scholar 

  • Siekmann, J., 1978: Unification and matching problems. Ph.D. thesis, Memo CSM-4-78, University of Essex.

    Google Scholar 

  • Siekmann, J., and Szabo, P., 1981: A Noetherian and confluent rewrite system for idempotent semigroups. SEKI-project memo, Univ. of Karlsruhe, FRG, Dep. Comp. Scie.

    Google Scholar 

  • Siekmann, J., and Szabo, P., 1982: Universal unification and classification of equational theories. Proc. 6th CADE (ed. by D.W. Loveland), Springer LNCS 138.

    Google Scholar 

  • Slagle, J.R., 1974: Automated theorem proving for theories with simplifiers, commutativity and associativity.

    Google Scholar 

  • Smith, D., 1966: A basis algorithm for finitely generated Abelian groups. Math. Algorithms 1/1, 13–26.

    Google Scholar 

  • Spear, D., 1977: A constructive approach to commutative ring theory. Proc. MACSYMA Users' Conf., Berkeley, July 1977, (ed. by R. J. Fateman), published by M.I.T., 369–376.

    Google Scholar 

  • Staples, J., 1975: Church-Rosser theorms for replacement systems. In: Algebra and Logic, (ed. by J. Crossley), Springer LN in Math., 291–307.

    Google Scholar 

  • Stickel, M.E., 1975: A complete unification algorithm for associative-commutative functions. Advance papers 4th Int. Joint Conf. on Artificial Intelligence, Tbilisi, USSR, pp. 71–76.

    Google Scholar 

  • Stickel, M.E., 1977: Unification algorithms for artificial intelligence languages. Ph.D. thesis, Carnegie-Mellon Univ.

    Google Scholar 

  • Stickel, M.E., 1981: A unification algorithm for associative commutative functions. J. ACM. 28/3, 423–434; preliminary version: 4th IJCAI, 1975.

    Google Scholar 

  • Stoutemyer, D.R., 1985: A preview of the next IBM-PC version of muMATH. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Szekeres, G., 1952: A canonical basis for the ideals of a polynomial domain. Am. Math. Monthly 59/6, 379–386.

    Google Scholar 

  • Thomas, C., 1984: RRLab — Rewrite Rule Labor. Memo SEKI-84-01, Fachbereich Informatik, Universität Kaiserslautern, Postfach 3049, D6750 Kaiserslautern.

    Google Scholar 

  • Tiden, E., Arnborg, S., 1985: Unification problems with one-sided distributivity. These proceedings.

    Google Scholar 

  • Trinks, W., 1978: On B. Buchberger's method for solving systems of algebraic equations (German). J. Number Theory, 10/4, 475–488.

    Google Scholar 

  • Winkler, F., 1978: Implementation of an algorithm for constructing Gröbner bases (German). Diploma thesis, Univ. of Linz, Austria (Europe), Math. Inst., to appear in ACM TOMS.

    Google Scholar 

  • Winkler, F., 1983: An algorithm for constructing detaching bases in the ring of polynomials over a field. Proc. EUROCAL 83, London, (ed. by J. A. van Hulzen), Springer LNCS 162, 168–179.

    Google Scholar 

  • Winkler, F., 1984: The Church-Rosser property in computer algebra and special theorem proving: an investigation of critical-pair/completion algorithms. Ph.D. thesis, Univ. of Linz, Austria (Europe), Math. Inst.

    Google Scholar 

  • Winkler, F., 1984a: On the complexity of the Gröbner-bases algorithm over K[x,y,z]. Proc. EUROSAM 84, Cambridge, (ed. by J. Fitch), Springer LNCS 174, 184–194.

    Google Scholar 

  • Winkler, F., 1985: Reducing the complexity of the Knuth-Bendix completion algorithm: a "unification" of different approaches. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Winkler, F., Buchberger, B., 1983: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. Proc. of the Coll. on Algebra, Combinatorics and Logic in Comp. Scie., Györ, to appear in Coll. Math. Soc. J. Bolyai, North-Holland.

    Google Scholar 

  • Wolf, T., 1985: Analytic decoupling, decision of compatibility and partial integration of systems of nonlinear ordinary and partial differential equations. Proc. EUROCAL 85, Springer LNCS, to appear.

    Google Scholar 

  • Wu, W., 1978: On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica 21/2, 159–172.

    Google Scholar 

  • Yellick, K., 1985: Combining unification algorithms for confined equational theories. These proceedings.

    Google Scholar 

  • Zacharias, G., 1978: Generalized Gröbner bases in commutative polynomial rings. Bachelor Thesis, M.I.T., Dept. Comp. Scie.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Johannes Kepler University, A4 040, Linz, Austria (Europe)

    Bruno Buchberger

Authors
  1. Bruno Buchberger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jean-Pierre Jouannaud

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Buchberger, B. (1985). Basic features and development of the critical-pair/completion procedure. 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_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-15976-2_1

  • 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

Publish with us

Policies and ethics

Search

Navigation