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
• 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

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)