Modular and incremental proofs of AC-termination

DOI10.1016/J.JSC.2004.02.003zbMath1137.68419OpenAlexW2031515077MaRDI QIDQ2643544

Claude Marché, Xavier Urbain

Publication date: 24 August 2007

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2004.02.003

zbMATH Keywords

rewritingterminationmodularityautomation

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42)

Related Items (12)

Relative termination via dependency pairs ⋮ Elimination transformations for associative-commutative rewriting systems ⋮ Twenty years of rewriting logic ⋮ AC-KBO revisited ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Enhancing dependency pair method using strong computability in simply-typed term rewriting ⋮ Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications ⋮ Automating the dependency pair method ⋮ Proving operational termination of membership equational programs ⋮ AC Completion with Termination Tools ⋮ Modular and incremental automated termination proofs

Uses Software

• OBJ3
• Maude
• CiME
• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination orderings for associative-commutative rewriting systems
• Termination of rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• Modularity of simple termination of term rewriting systems with shared constructors
• Generalized sufficient conditions for modular termination of rewriting
• On the modularity of termination of term rewriting systems
• Modular proofs for completeness of hierarchical term rewriting systems
• Maude: specification and programming in rewriting logic
• Hierarchical termination revisited.
• Context-sensitive rewriting strategies
• Modular termination proofs for rewriting using dependency pairs
• Modular properties of composable term rewriting systems
• Termination of term rewriting using dependency pairs
• Completeness of combinations of constructor systems
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Modular and incremental automated termination proofs
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Rewrite systems for natural, integral, and rational arithmetic
• A total, ground path ordering for proving termination of AC-rewrite systems
• Extension of the associative path ordering to a chain of associative commutative symbols

This page was built for publication: Modular and incremental proofs of AC-termination