Completion of a Set of Rules Modulo a Set of Equations
From MaRDI portal
Publication:3816048
DOI10.1137/0215084zbMath0665.03005OpenAlexW2042924775MaRDI QIDQ3816048
Hélène Kirchner, Jean-Pierre Jouannaud
Publication date: 1986
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/0215084
decidabilityequivalence relationcompletion procedureChurch-Rosser propertyreduction relationequivalence congruence classes of terms of a free algebraterminating rewriting systems
Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) Equational logic, Mal'tsev conditions (08B05) Equational classes, universal algebra in model theory (03C05)
Related Items
Meta-rule synthesis from crossed rewrite systems, Completion procedures as semidecision procedures, An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis, Unification in varieties of completely regular semigroups, Local confluence of conditional and generalized term rewriting systems, Functional Logic Programming in Maude, Unification theory, AC-superposition with constraints: No AC-unifiers needed, On pot, pans and pudding or how to discover generalised critical Pairs, On solving the equality problem in theories defined by Horn clauses, Unnamed Item, Non-disjoint combined unification and closure by equational paramodulation, Automated deduction with associative-commutative operators, Complete sets of reductions modulo associativity, commutativity and identity, Abstract rewriting with concrete operators, On how to move mountains ‘associatively and commutatively’, Undecidable properties of syntactic theories, Decidability of confluence and termination of monadic term rewriting systems, Proving equational and inductive theorems by completion and embedding techniques, Simulating Buchberger's algorithm by Knuth-Bendix completion, On ground AC-completion, Open problems in rewriting, Bi-rewriting, a term rewriting technique for monotonic order relations, A case study of completion modulo distributivity and Abelian groups, More problems in rewriting, AC-complete unification and its application to theorem proving, Buchberger's algorithm: The term rewriter's point of view, Termination of rewriting, Structures for abstract rewriting, Modular and incremental proofs of AC-termination, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Critical pair criteria for completion, Preperfectness is undecidable for Thue systems containing only length- reducing rules and a single commutation rule, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, A \(\rho\)-calculus of explicit constraint application, On confluence versus strong confluence for one-rule trace-rewriting systems, Metalevel algorithms for variant satisfiability, On First-Order Model-Based Reasoning, Normal Higher-Order Termination, Optimization of rewriting and complexity of rewriting, AC-Termination of rewrite systems: A modified Knuth-Bendix ordering, Unification properties of commutative theories: A categorical treatment, Buchberger's algorithm: A constraint-based completion procedure, Higher-order narrowing with convergent systems, From diagrammatic confluence to modularity, One-rule trace-rewriting systems and confluence, Abstract data type systems, Twenty years of rewriting logic, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Drags: a compositional algebraic framework for graph rewriting, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Unification of drags and confluence of drag rewriting, Deciding the word problem in the union of equational theories., A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., A Completion Method to Decide Reachability in Rewrite Systems, Linear-algebraic λ-calculus: higher-order, encodings, and confluence., Equational completion in order-sorted algebras, A rewriting strategy to verify observational congruence, Unification in commutative rings is not finitary, Unnamed Item, Unnamed Item, Theorem proving modulo, Computing knowledge in equational extensions of subterm convergent theories, On the unification problem for Cartesian closed categories, Conditional congruence closure over uninterpreted and interpreted symbols, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, Specification and proof in membership equational logic, Semantics of order-sorted specifications, Combining matching algorithms: The regular case, A semantic framework for open processes, Towards a foundation of completion procedures as semidecision procedures, Conditional rewriting logic as a unified model of concurrency, Strict coherence of conditional rewriting modulo axioms, Termination and completion modulo associativity, commutativity and identity, The vectorial \(\lambda\)-calculus, Process algebra with strategic interleaving, Combining matching algorithms: The regular case, Abstract canonical presentations, Superposition theorem proving for abelian groups represented as integer modules, Unification in commutative theories, Unification in a combination of arbitrary disjoint equational theories, Any ground associative-commutative theory has a finite canonical system, Variant-Based Satisfiability in Initial Algebras, Normal forms and normal theories in conditional rewriting, Generalized rewrite theories, coherence completion, and symbolic methods, Conditional narrowing modulo a set of equations, Completion for rewriting modulo a congruence, Schematization of infinite sets of rewrite rules generated by divergent completion processes, On deciding confluence of finite string-rewriting systems modulo partial commutativity, Extending Maximal Completion (Invited Talk), Superposition theorem proving for abelian groups represented as integer modules, Metalevel Algorithms for Variant Satisfiability, Automatic proofs by induction in theories without constructors, Unification in permutative equational theories is undecidable, Inductive proof search modulo, Termination Modulo Combinations of Equational Theories, Swinging types=functions+relations+transition systems, Partial completion of equational theories, Unions of non-disjoint theories and combinations of satisfiability procedures, Set of support, demodulation, paramodulation: a historical perspective, Refutational theorem proving using term-rewriting systems, Towards a Sharing Strategy for the Graph Rewriting Calculus, ELAN from a rewriting logic point of view, Maude: specification and programming in rewriting logic, Equational rules for rewriting logic, Abstract abstract reduction, Symbolic computation in Maude: some tapas, Pattern eliminating transformations, Terminating non-disjoint combined unification
