Termination Analysis by Dependency Pairs and Inductive Theorem Proving

DOI10.1007/978-3-642-02959-2_25zbMath1237.68181OpenAlexW1892882113MaRDI QIDQ5191111

Michael Parting, Jürgen Giesl, Stephan Swiderski, Carsten Fuhs, Peter Schneider-Kamp

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_25

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (1)

Proving termination by dependency pairs and inductive theorem proving

Uses Software

• Haskell
• Tyrolean
• AProVE
• SPIKE
• VeriFun

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Proof by consistency
• Termination of term rewriting: Interpretation and type elimination
• On proving the termination of algorithms by machine
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• Termination of rewriting under strategies
• Automated termination proofs for logic programs by term rewriting
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Proving Termination by Bounded Increase
• Certified Size-Change Termination
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Term Rewriting and All That
• Logic for Programming, Artificial Intelligence, and Reasoning
• Termination Analysis with Calling Context Graphs
• Termination of logic programs: Transformational methods revisited

This page was built for publication: Termination Analysis by Dependency Pairs and Inductive Theorem Proving