Modular and incremental proofs of AC-termination

DOI10.1016/J.JSC.2004.02.003zbMATH Open1137.68419OpenAlexW2031515077MaRDI QIDQ2643544FDOQ2643544

Authors: 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

Recommendations

• Modular and incremental automated termination proofs
• Termination Modulo Combinations of Equational Theories
• scientific article; zbMATH DE number 4047066
• scientific article; zbMATH DE number 1765695
• AC dependency pairs revisited

zbMATH Keywords

modularityautomationrewritingtermination

Mathematics Subject Classification ID

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

Cites Work

• Maude: specification and programming in rewriting logic
• Termination of rewriting systems by polynomial interpretations and its implementation
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Termination of rewriting
• Complete Sets of Reductions for Some Equational Theories
• Termination orderings for associative-commutative rewriting systems
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Title not available (Why is that?)
• Rewrite systems for natural, integral, and rational arithmetic
• Title not available (Why is that?)
• Modular properties of composable term rewriting systems
• Title not available (Why is that?)
• Counterexamples to termination for the direct sum of term rewriting systems
• Context-sensitive rewriting strategies
• Completion of a Set of Rules Modulo a Set of Equations
• 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
• Completeness of combinations of constructor systems
• Title not available (Why is that?)
• Extension of the associative path ordering to a chain of associative commutative symbols
• Title not available (Why is that?)
• Modular proofs for completeness of hierarchical term rewriting systems
• Hierarchical termination revisited.
• Title not available (Why is that?)
• Modular and incremental automated termination proofs
• Title not available (Why is that?)
• A total, ground path ordering for proving termination of AC-rewrite systems
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (14)

• Twenty years of rewriting logic
• Stability of termination and sufficient-completeness under pushouts via amalgamation
• Proving operational termination of membership equational programs
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Automating the dependency pair method
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Relative termination via dependency pairs
• Elimination transformations for associative-commutative rewriting systems
• AC-KBO revisited
• Automated Reasoning
• Modular and incremental automated termination proofs
• Title not available (Why is that?)
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• AC completion with termination tools

Uses Software

• OBJ3
• Maude
• CiME
• REVE

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2643544)