scientific article
From MaRDI portal
Publication:3745825
zbMath0607.03003MaRDI QIDQ3745825
Bruno Buchberger, Franz Winkler
Publication date: 1986
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
equational theoryword problemscompletion procedureChurch-Rosser propertyreduction relationsgeneralized Newman lemma
Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05)
Related Items
New constructive methods in classical ideal theory ⋮ Consider only general superpositions in completion procedures ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ 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 ⋮ Sufficient set of integrability conditions of an orthonomic system ⋮ Unnecessary inferences in associative-commutative completion procedures ⋮ Confluence by Decreasing Diagrams ⋮ An algorithm for the construction of matrix representations for finitely presented non-commutative algebras ⋮ Order-sorted completion: The many-sorted way ⋮ Redundancy criteria for constrained completion ⋮ Redundancy criteria for constrained completion ⋮ On pot, pans and pudding or how to discover generalised critical Pairs ⋮ Unnamed Item ⋮ Gröbner-Shirshov basis for the braid group in the Birman-Ko-Lee generators. ⋮ Mathematical Theory Exploration in Theorema: Reduction Rings ⋮ Diagram techniques for confluence ⋮ A completion procedure for conditional equations ⋮ Refutational theorem proving using term-rewriting systems ⋮ Gröbner bases in orders of algebraic number fields. ⋮ Multi-valued logic and Gröbner bases with applications to modal logic ⋮ Elimination of composite superpositions may cause abortion
