On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs

DOI10.1007/978-3-642-22531-4_9MaRDI QIDQ5200103zbMATH OpenOpenAlexFDO

Authors Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe

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)

Recommendations

• Beyond Dependency Graphs
• Termination of term rewriting using dependency pairs
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Improving dependency pairs
• Termination by absence of infinite chains of dependency pairs

Cites work

• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Automated Induction with Constrained Tree Automata
• Automating the dependency pair method.
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Completion of rewrite systems with membership constraints. II: Constraint solving
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 4092756 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• scientific article; zbMATH DE number 1446599 (Why is no real title available?)
• Implicit induction in conditional theories
• Incorporating decision procedures in implicit induction.
• Inductive Decidability Using Implicit Induction
• Logic for Programming, Artificial Intelligence, and Reasoning
• Maximal Termination
• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• Orderings and Constraints: Theory and Practice of Proving Termination
• Proving Termination by Bounded Increase
• Proving Termination of Integer Term Rewriting
• Redundancy criteria for constrained completion
• Term Rewriting and All That
• Termination of term rewriting using dependency pairs
• Tyrolean termination tool: techniques and features

Cited in

(6)

• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Rewriting modulo SMT and open system analysis
• Certifying a Termination Criterion Based on Graphs, without Graphs
• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• Verifying procedural programs via constrained rewriting induction
• A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems

Describes a project that uses

Uses Software

• AProVE
• Tyrolean

This page was built for publication: On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs

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