scientific article; zbMATH DE number 3981150

MaRDI QIDQ3745825zbMATH OpenFDO

Authors Bruno Buchberger, Franz Winkler

Publication date 1986

zbMATH Keywords

Church-Rosser propertycompletion procedureequational theorygeneralized Newman lemmareduction relationsword problems

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05)

Recommendations

• scientific article; zbMATH DE number 4016226
• scientific article; zbMATH DE number 3928345
• scientific article; zbMATH DE number 3928346
• scientific article; zbMATH DE number 44069
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure

Cited in

(31)

• Gröbner-Shirshov basis for the braid group in the Birman-Ko-Lee generators.
• New constructive methods in classical ideal theory
• History and basic features of the critical-pair/completion procedure
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• A generalization of reduction rings
• Order-sorted completion: The many-sorted way
• Diagram techniques for confluence
• Buchberger's algorithm: The term rewriter's point of view
• Gröbner bases in orders of algebraic number fields.
• Detecting unnecessary reductions in an involutive basis computation
• Sufficient set of integrability conditions of an orthonomic system
• Mathematical theory exploration in Theorema: reduction rings
• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• Unnecessary inferences in associative-commutative completion procedures
• Confluence by Decreasing Diagrams
• scientific article; zbMATH DE number 3928345 (Why is no real title available?)
• scientific article; zbMATH DE number 3928346 (Why is no real title available?)
• Groebner_Bases
• Consider only general superpositions in completion procedures
• Redundancy criteria for constrained completion
• scientific article; zbMATH DE number 7204438 (Why is no real title available?)
• On pot, pans and pudding or how to discover generalised critical pairs
• Complete sets of reductions with constraints
• Redundancy criteria for constrained completion
• Rewriting modulo in diagrammatic algebras and application to categorification
• A completion procedure for conditional equations
• Refutational theorem proving using term-rewriting systems
• Multi-valued logic and Gröbner bases with applications to modal logic
• Elimination of composite superpositions may cause abortion
• An algorithm for the construction of matrix representations for finitely presented non-commutative algebras

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3745825)