Automated incremental termination proofs for hierarchically defined term rewriting systems

DOI10.1007/3-540-45744-5_42MaRDI QIDQ4539636zbMATH OpenFDO

Authors Xavier Urbain

Publication date 10 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2083/20830485

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Modular and incremental automated termination proofs
• Modular and incremental proofs of AC-termination
• Modular termination proofs for rewriting using dependency pairs
• Dependency pairs for equational rewriting
• Termination of term rewriting using dependency pairs

Cited in

(11)

• Modular proofs for completeness of hierarchical term rewriting systems
• Hierarchical termination revisited.
• Modular termination proofs for rewriting using dependency pairs
• Proving operational termination of membership equational programs
• Modular and incremental automated termination proofs
• Modular and incremental proofs of AC-termination
• Real_Impl
• Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
• Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting (invited talk)
• On proving \(C_E\)-termination of rewriting by size-change termination
• Elimination transformations for associative-commutative rewriting systems

This page was built for publication: Automated incremental termination proofs for hierarchically defined term rewriting systems

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