Modular and incremental automated termination proofs

DOI10.1007/BF03177743zbMath1096.68076MaRDI QIDQ2583289

Xavier Urbain

Publication date: 16 January 2006

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

rewriting modules

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Mechanically proving termination using polynomial interpretations, Modular and incremental proofs of AC-termination, Proving termination of context-sensitive rewriting by transformation, Tyrolean termination tool: techniques and features, Elimination transformations for associative-commutative rewriting systems, Mechanizing and improving dependency pairs, Twenty years of rewriting logic, Modular Termination of Basic Narrowing, Usable Rules for Context-Sensitive Rewrite Systems, 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, Proving operational termination of membership equational programs, Argument Filterings and Usable Rules for Simply Typed Dependency Pairs

Uses Software

• AProVE
• Tsukuba

Cites Work

• Mechanically proving termination using polynomial interpretations
• Termination of rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• On termination of the direct sum of term-rewriting systems
• Generating polynomial orderings
• 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
• Modular properties of composable term rewriting systems
• Termination of term rewriting using dependency pairs
• Completeness of combinations of constructor systems
• Modular and incremental proofs of AC-termination
• Induction for termination with local strategies
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item