Modular and incremental proofs of AC-termination

DOI10.1016/J.JSC.2004.02.003MaRDI QIDQ2643544zbMATHOpenAlexFDO

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

zbMATH Keywords

modularityautomationrewritingtermination

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 1722701 (Why is no real title available?)
• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 2043535 (Why is no real title available?)
• scientific article; zbMATH DE number 1479616 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• scientific article; zbMATH DE number 1507181 (Why is no real title available?)
• scientific article; zbMATH DE number 1765695 (Why is no real title available?)
• scientific article; zbMATH DE number 1405623 (Why is no real title available?)
• A total, ground path ordering for proving termination of AC-rewrite systems
• Complete Sets of Reductions for Some Equational Theories
• Completeness of combinations of constructor systems
• Completion of a Set of Rules Modulo a Set of Equations
• Context-sensitive rewriting strategies
• Counterexamples to termination for the direct sum of term rewriting systems
• Extension of the associative path ordering to a chain of associative commutative symbols
• Generalized sufficient conditions for modular termination of rewriting
• Hierarchical termination revisited.
• Maude: specification and programming in rewriting logic
• Modular and incremental automated termination proofs
• Modular proofs for completeness of hierarchical term rewriting systems
• Modular properties of composable term rewriting systems
• Modular termination proofs for rewriting using dependency pairs
• Modularity of simple termination of term rewriting systems with shared constructors
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• On the modularity of termination of term rewriting systems
• Rewrite systems for natural, integral, and rational arithmetic
• Termination of rewriting
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination of term rewriting using dependency pairs
• Termination orderings for associative-commutative rewriting systems

Cited in

(15)

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

Describes a project that uses

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)