scientific article; zbMATH DE number 3299786

zbMATH Open0188.04902MaRDI QIDQ5581665FDOQ5581665

Authors: Donald E. Knuth, P. B. Bendix 

Publication date: 1970

Title of this publication is not available (Why is that?)

zbMATH Keywords

general algebraic structures

Cited In (only showing first 100 items - show all)

• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Conjecture synthesis for inductive theories
• Termination proofs and the length of derivations
• Set-theoretic graph rewriting
• Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent
• String rewriting for double coset systems.
• Unification theory
• Boolean algebra admits no convergent term rewriting system
• Semantic foundations for generalized rewrite theories
• Pseudo-natural algorithms for the word problem for finitely presented monoids and groups
• A catalogue of complete group presentations
• Complexity of matching problems
• Effective codescent morphisms in the varieties determined by convergent term rewriting systems.
• Orderings for term-rewriting systems
• Automating theories in intuitionistic logic
• Rewriting systems of Coxeter groups
• Interpolation and Symbol Elimination
• Proofs by induction in equational theories with constructors
• Refutational theorem proving using term-rewriting systems
• Adding decision procedures to SMT solvers using axioms with triggers
• Higher-order rewrite systems and their confluence
• The diamond lemma for ring theory
• Complete sets of reductions modulo associativity, commutativity and identity
• Polynomials over the reals in proofs of termination : from theory to practice
• On ground-confluence of term rewriting systems
• Decreasing diagrams and relative termination
• Decreasing diagrams and relative termination
• On deciding satisfiability by theorem proving with speculative inferences
• On sufficient-completeness and related properties of term rewriting systems
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Best unifiers in transitive modal logics
• Towards a foundation of completion procedures as semidecision procedures
• Finite derivation type for semilattices of semigroups.
• On word problems in Horn theories
• Theorem-proving with resolution and superposition
• Multi-completion with Termination Tools (System Description)
• Unification in a combination of arbitrary disjoint equational theories
• KBO orientability
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Gröbner-Shirshov bases and their calculation
• Decidability of elementary theories of certain finitely defined algebras
• Complexity of unification problems with associative-commutative operators
• Proof by consistency
• Termination of rewriting
• Automated proofs of the Moufang identities in alternative rings
• Modular termination proofs for rewriting using dependency pairs
• Deciding confluence of certain term rewriting systems in polynomial time
• New methods for using Cayley graphs in interconnection networks
• Termination orderings for associative-commutative rewriting systems
• Embedding Boolean expressions into logic programming
• Termination of term rewriting using dependency pairs
• A generalization of the matrix equation \(A^ 2=J\)
• Learning domain knowledge to improve theorem proving
• A rewriting approach to satisfiability procedures.
• Termination and completion modulo associativity, commutativity and identity
• Efficiently solving quantified bit-vector formulas
• Algebraic properties of some quadratic dynamical systems
• Confluent linear numeration systems
• How to prove decidability of equational theories with second-order computation analyser SOL
• Single axioms for groups and abelian groups with various operations
• The shortest single axioms for groups of exponent 4
• A finite Thue system with decidable word problem and without equivalent finite canonical system
• Completion for multiple reduction orderings
• An application of matrix theory to a problem in universal algebra
• Undecidable properties on length-two string rewriting systems
• Sufficient-completeness, ground-reducibility and their complexity
• AC-termination of rewrite systems: a modified Knuth-Bendix ordering
• Gröbner-Shirshov bases, conformal algebras, and pseudo-algebras.
• Multi-completion with termination tools
• The word problem for finitely presented quandles is undecidable
• Attributed graph transformation with inheritance: efficient conflict detection and local confluence analysis using abstract critical pairs
• Computing a Gröbner basis of a polynomial ideal over a Euclidean domain
• Derivation lengths and order types of Knuth--Bendix orders
• Completion for constrained term rewriting systems
• Gröbner-Shirshov bases for associative algebras with multiple operators and free Rota-Baxter algebras.
• Knuth-Bendix completion of theories of commuting group endomorphisms
• Mechanizing and improving dependency pairs
• Theorem proving modulo
• A rationale for conditional equational programming
• Polygraphs of finite derivation type
• Conditional rewrite rules
• On the connection between narrowing and proof by consistency
• Critical pair criteria for completion
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Deciding knowledge in security protocols under some e-voting theories
• A unifying splitting framework
• Church-Rosser systems with respect to formal languages
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Proving Confluence of Term Rewriting Systems Automatically
• Reduction operators and completion of rewriting systems
• Termination tools in ordered completion
• On graph rewritings
• Term rewriting induction
• Deductive and inductive synthesis of equational programs
• More efficient bottom-up multi-pattern matching in trees
• On weakly confluent monadic string-rewriting systems
• Solving divergence in Knuth--Bendix completion by enriching signatures
• Using geometric rewrite rules for solving geometric problems symbolically
• Confluence by critical pair analysis revisited
• Rewrite method for theorem proving in first order theory with equality

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 Q5581665)