On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs

DOI10.1007/978-3-642-22531-4_9zbMath1339.68141OpenAlexW5060831MaRDI QIDQ5200103

Toshiki Sakabe, Tsubasa Sakata, Naoki Nishida

Publication date: 29 July 2011

Published in: Functional and Constraint Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22531-4_9

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (4)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Rewriting modulo SMT and open system analysis ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs

Uses Software

• Tyrolean
• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Redundancy criteria for constrained completion
• Tyrolean termination tool: techniques and features
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Completion of rewrite systems with membership constraints. II: Constraint solving
• Incorporating decision procedures in implicit induction.
• Implicit induction in conditional theories
• Termination of term rewriting using dependency pairs
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Maximal Termination
• Automated Induction with Constrained Tree Automata
• Proving Termination by Bounded Increase
• Orderings and Constraints: Theory and Practice of Proving Termination
• Proving Termination of Integer Term Rewriting
• Term Rewriting and All That
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs
• Inductive Decidability Using Implicit Induction
• Logic for Programming, Artificial Intelligence, and Reasoning
• Automated Deduction – CADE-19

This page was built for publication: On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs