On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs
From MaRDI portal
Publication:5200103
DOI10.1007/978-3-642-22531-4_9zbMath1339.68141MaRDI 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
68Q42: Grammars and rewriting systems
Related Items
On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs, Verifying Procedural Programs via Constrained Rewriting Induction, Rewriting modulo SMT and open system analysis, From Jinja bytecode to term rewriting: a complexity reflecting transformation
Uses Software
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