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)

• Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
• The problem of demodulator adjunction
• Iterating transducers
• Title not available (Why is that?)
• Decision problems for finite special string-rewriting systems that are confluent on some congruence class
• Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm
• On the Coalgebra of Partial Differential Equations
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
• Loops with abelian inner mapping groups: an application of automated deduction
• Performance of clause selection heuristics for saturation-based theorem proving
• Orienting rewrite rules with the Knuth-Bendix order.
• Proving termination of context-sensitive rewriting by transformation
• Representing and building models for decidable subclasses of equational clausal logic
• Things to know when implementing KBO
• A notation for lambda terms. A generalization of environments
• On the duality of abduction and model generation in a framework for model generation with equality
• Proof normalization for resolution and paramodulation
• Proving termination of (conditional) rewrite systems. A semantic approach
• Superposition-based equality handling for analytic tableaux
• Resolution with order and selection for hybrid logics
• Comparing data type specifications via their normal forms
• On proving properties of completion strategies
• Finite complete rewriting systems and the complexity of word problem
• Relating rewriting techniques on monoids and rings: congruences on monoids and ideals in monoid rings
• Clausal rewriting
• Automating the Knuth Bendix ordering
• Automating inductionless induction using test sets
• On the relation between resolution based and completion based theorem proving
• Weights for total division orderings on strings
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Rewrite systems on a lattice of types
• Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
• Remarks on an example of Jantzen
• Unification in permutative equational theories is undecidable
• Confluence of algebraic rewriting systems
• About the descriptive power of certain classes of finite string-rewriting systems
• Equational completion in order-sorted algebras
• An algorithm for the construction of matrix representations for finitely presented non-commutative algebras
• Reductions in tree replacement systems
• n-level rewriting systems
• A class of confluent term rewriting systems and unification
• History and basic features of the critical-pair/completion procedure
• Pseudo-natural algorithms for finitely generated presentations of monoids and groups
• Semantics of order-sorted specifications
• The Knuth-Bendix procedure for strings as a substitute for coset enumeration
• Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited
• The Church-Rosser property for ground term-rewriting systems is decidable
• Completion for logically constrained rewriting
• Hereditarily finitely generated commutative monoids
• The size-change principle and dependency pairs for termination of term rewriting
• Regaining cut admissibility in deduction modulo using abstract completion
• Order-Sorted Rewriting and Congruence Closure
• Partial completion of equational theories
• A systematic study of models of abstract data types
• Modular tree transducers
• Semi-unification
• Finite generation of ambiguity in context-free languages
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Unique normal forms for nonlinear term rewriting systems: Root overlaps
• 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

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)