Buchberger's algorithm: A constraint-based completion procedure

DOI10.1007/BFb0016860zbMath1495.68249MaRDI QIDQ5096314

Leo Bachmair, Harald Ganzinger

Publication date: 16 August 2022

Published in: Constraints in Computational Logics (Search for Journal in Brave)

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Related Items

Buchberger's algorithm: The term rewriter's point of view, A new symbolic method for solving linear two-point boundary value problems on the level of operators, A search-based procedure for nonlinear real arithmetic, A general framework to build contextual cover set induction provers

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Refutational theorem proving using term-rewriting systems
• Termination orderings for associative-commutative rewriting systems
• History and basic features of the critical-pair/completion procedure
• Computing a Gröbner basis of a polynomial ideal over a Euclidean domain
• Refutational theorem proving for hierarchic first-order theories
• A new method for the Boolean ring based theorem proving
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Equational inference, canonical proofs, and proof orderings
• Rewrite-based Equational Theorem Proving with Selection and Simplification