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)

• 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
• Meta-rule synthesis from crossed rewrite systems
• A superposition oriented theorem prover
• Some results on the confluence property of combined term rewriting systems
• Thue systems as rewriting systems
• Implementing first-order rewriting with constructor systems
• Operational semantics of a kernel of the language ELECTRE
• Complete sets of reductions with constraints
• On restrictions of ordered paramodulation with simplification
• Complete equational unification based on an extension of the Knuth-Bendix completion procedure
• Completion for rewriting modulo a congruence
• Complete sets of transformations for general E-unification
• Any ground associative-commutative theory has a finite canonical system
• A refinement of strong sequentiality for term rewriting with constructors
• Ordered rewriting and confluence
• Rippling: A heuristic for guiding inductive proofs
• Schematization of infinite sets of rewrite rules generated by divergent completion processes
• A completion-based method for mixed universal and rigid \(E\)-unification
• CSI -- a confluence tool
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Gröbner-Shirshov basis for the braid group in the Birman-Ko-Lee generators.
• An improved general path order
• Properties of graphs preserved by relational graph rewritings
• On recursive path ordering
• Conditions for confluence of innermost terminating term rewriting systems
• Lifting canonical algorithms from a ring R to the ring R[x]
• Building exact computation sequences
• Verifying nilpotence
• Order-sorted unification
• Composition-diamond lemma for associative conformal algebras.
• Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
• Decidable sentences of Church-Rosser congruences
• Higher-order substitutions
• Unification in combinations of collapse-free regular theories
• On deciding the confluence of a finite string-rewriting system on a given congruence class
• New decision algorithms for finitely presented commutative semigroups
• A Noetherian and confluent rewrite system for idempotent semigroups
• Automatic proofs by induction in theories without constructors
• Non-resolution theorem proving
• Structures for abstract rewriting
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• A note on simplification orderings
• Testing for the Church-Rosser property
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• A compact fixpoint semantics for term rewriting systems
• Unnecessary inferences in associative-commutative completion procedures
• Complete sets of unifiers and matchers in equational theories
• Categorification, term rewriting and the Knuth-Bendix procedure
• Complete involutive rewriting systems
• Infinite trees in normal form and recursive equations having a unique solution
• Finite complete rewriting systems for the Jantzen monoid and the Greendlinger group
• Rewrite systems for varieties of semigroups
• A PVS theory for term rewriting systems
• Reachability analysis over term rewriting systems
• The problems of cyclic equality and conjugacy for finite complete rewriting systems
• Efficiency issues in the KBMAG procedure
• Induction using term orderings
• On the data type extension problem for algebraic specifications
• Consider only general superpositions in completion procedures
• Incremental termination proofs and the length of derivations
• Topics in termination
• On proving confluence modulo equivalence for Constraint Handling Rules
• Title not available (Why is that?)
• Complete positive group presentations.
• Simulating Buchberger's algorithm by Knuth-Bendix completion
• Rewrite rules for \(\mathrm{CTL}^\ast\)
• A strong restriction of the inductive completion procedure
• A general framework to build contextual cover set induction provers
• A geometrical approach to multiset orderings
• Rigid E-unification: NP-completeness and applications to equational matings
• Confluence for graph transformations
• Natural termination
• Relational graph rewritings
• Completion of first-order clauses with equality by strict superposition
• Using forcing to prove completeness of resolution and paramodulation
• 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

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)