Termination Analysis by Dependency Pairs and Inductive Theorem Proving

DOI10.1007/978-3-642-02959-2_25MaRDI QIDQ5191111zbMATH OpenOpenAlexFDO

Authors Stephan Swiderski, Michael Parting, Jürgen Giesl, 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)

Recommendations

• Proving termination by dependency pairs and inductive theorem proving
• Logic for Programming, Artificial Intelligence, and Reasoning
• Automated Reasoning
• Improving dependency pairs
• Termination of term rewriting using dependency pairs

Cites work

• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated termination proofs for logic programs by term rewriting
• Automating the dependency pair method
• Certified Size-Change Termination
• scientific article; zbMATH DE number 4074541 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 794237 (Why is no real title available?)
• Inductionless induction
• Logic for Programming, Artificial Intelligence, and Reasoning
• Mechanizing and improving dependency pairs
• On proving the termination of algorithms by machine
• Proof by consistency
• Proving Termination by Bounded Increase
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Term Rewriting and All That
• Termination Analysis with Calling Context Graphs
• Termination of logic programs: Transformational methods revisited
• Termination of rewriting under strategies
• Termination of term rewriting using dependency pairs
• Termination of term rewriting: Interpretation and type elimination
• The automation of proof by mathematical induction
• Tyrolean termination tool: techniques and features

Cited in

(16)

• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Dynamic dependency pairs for algebraic functional systems
• Termination Competition (termCOMP 2015)
• TPA: Termination Proved Automatically
• Proving Termination by Bounded Increase
• All-Termination(T)
• Proving Termination of Integer Term Rewriting
• scientific article; zbMATH DE number 4072437 (Why is no real title available?)
• Proving termination by dependency pairs and inductive theorem proving
• scientific article; zbMATH DE number 2043537 (Why is no real title available?)
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Automated Reasoning
• Term Rewriting and Applications
• Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday
• Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
• Tyrolean termination tool: techniques and features

Describes a project that uses

Uses Software

• AProVE
• Haskell
• Tyrolean
• SPIKE
• VeriFun

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

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