History and basic features of the critical-pair/completion procedure

DOI10.1016/S0747-7171(87)80020-2zbMath0645.68094MaRDI QIDQ1103414

Bruno Buchberger

Publication date: 1987

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

surveyGröbner basisterminationefficient implementationBuchberger algorithmrecursive predicatescritical-pair/completionmodel semanticsrule rewriting transformations

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Formal languages and automata (68Q45) Research exposition (monographs, survey articles) pertaining to history and biography (01-02) History of computer science (68-03) Word problems (aspects of algebraic structures) (08A50)

Related Items

An equational logic sampler, Parallel dynamic semantics of sequential programs with speculative and incremental computation, Parallelization of the Buchberger algorithm, Reduction operators and completion of rewriting systems, Unification theory, Algorithmic operator algebras via normal forms in tensor rings, From LP to LP: Programming with constraints, Buchberger's algorithm: A constraint-based completion procedure, Locking-free compressible quadrilateral finite elements: Poisson's ratio-dependent vector interpolants, Gröbner-Shirshov bases for the non-symmetric operads of dendriform algebras and quadri-algebras, Automated proof of ring commutativity problems by algebraic methods, A survey on signature-based algorithms for computing Gröbner bases, From Analytical Mechanics Problems to Rewriting Theory Through M. Janet’s Work, Noncommutative Gröbner Bases: Applications and Generalizations, Some experiments with a completion theorem prover, A field guide to equational logic, Standard Gröbner-Shirshov Bases of Free Algebras Over Rings, I, Some categories associated with bases of the Kalman algebra, How to decide the lark, Gröbner–Shirshov bases and their calculation, Convergent presentations and polygraphic resolutions of associative algebras, Abstract canonical presentations, On equational theories, unification, and (un)decidability, A categorical critical-pair completion algorithm, Automated inferencing

Uses Software

• IBM Scratchpad
• REDUCE
• RRL
• AFFIRM
• REVE
• NARROWER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Testing for the Church-Rosser Property
• Word problems
• A computer application to finite p-groups
• A Machine-Oriented Logic Based on the Resolution Principle
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Notes on central groupoids
• An Abstract form of the church-rosser theorem. I
• Tree-Manipulating Systems and Church-Rosser Theorems
• Some Properties of Conversion
• The Word Problem for Abstract Algebras
• A Canonical Basis for the Ideals of a Polynomial Domain
• Orderings for term-rewriting systems
• Proofs by induction in equational theories with constructors
• Finite complete rewriting systems and the complexity of word problem
• MACSYMA from F to G
• Equational methods in first order predicate calculus
• Termination orderings for associative-commutative rewriting systems
• A note on simplification orderings
• New decision algorithms for finitely presented commutative semigroups
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• On multiset orderings
• A Noetherian and confluent rewrite system for idempotent semigroups
• Mehrdimensionale Hermite-Interpolation und numerische Integration
• The diamond lemma for ring theory
• An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
• Über B. Buchbergers Verfahren, Systeme algebraischer Gleichungen zu lösen
• Théorème de division et stabilité en géométrie analytique locale
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
• Resolution of singularities of an algebraic variety over a field of characteristic zero. I
• Über die Eliminationstheorie
• On theories with a combinatorial definition of 'equivalence'
• An improved algorithmic construction of Gröbner-bases for polynomial ideals
• An improved proof procedure1
• Dehn's algorithm for the word problem
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Proving termination with multiset orderings
• Abstract Data Type Specification in the Affirm System
• A simplified proof of the characterization theorem for Gröbner-bases
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• Confluent and Other Types of Thue Systems
• Complete Sets of Reductions for Some Equational Theories
• An abstract Church-Rosser theorem. II: Applications
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity