Completion for rewriting modulo a congruence

From MaRDI portal
Publication:1262752

DOI10.1016/0304-3975(89)90003-0zbMath0686.68021OpenAlexW1589182689MaRDI QIDQ1262752

Nachum Dershowitz, Leo Bachmair

Publication date: 1989

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90003-0




Related Items

Automated deduction with associative-commutative operatorsCoherent confluence modulo relations and double groupoidsDecidability of confluence and termination of monadic term rewriting systemsProving equational and inductive theorems by completion and embedding techniquesSimulating Buchberger's algorithm by Knuth-Bendix completionBi-rewriting, a term rewriting technique for monotonic order relationsExplicit substitutions with de bruijn's levelsAC-complete unification and its application to theorem provingString Diagram Rewrite Theory I: Rewriting with Frobenius StructureInfinite complete group presentationsBuchberger's algorithm: The term rewriter's point of viewOn the Church-Rosser and coherence properties of conditional order-sorted rewrite theoriesA rewriting strategy to verify observational congruenceTowards a foundation of completion procedures as semidecision proceduresStrict coherence of conditional rewriting modulo axiomsTermination and completion modulo associativity, commutativity and identityAC-superposition with constraints: No AC-unifiers neededA completion-based method for mixed universal and rigid E-unificationEquational theorem proving moduloExtending Maximal Completion (Invited Talk)Termination Modulo Combinations of Equational TheoriesPartial completion of equational theoriesDeduction, Strategies, and RewritingConfluence of algebraic rewriting systems


Uses Software


Cites Work