Proving termination by dependency pairs and inductive theorem proving
From MaRDI portal
Publication:438537
DOI10.1007/s10817-010-9215-9zbMath1243.68267OpenAlexW2094896759MaRDI QIDQ438537
Jürgen Giesl, Peter Schneider-Kamp, Stephan Swiderski, Michael Parting, Carsten Fuhs
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9215-9
Related Items (5)
Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Pattern eliminating transformations
Uses Software
Cites Work
- Termination of rewriting systems by polynomial interpretations and its implementation
- KBO orientability
- Tyrolean termination tool: techniques and features
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- On sufficient-completeness and related properties of term rewriting systems
- Proof by consistency
- Counterexamples to termination for the direct sum of term rewriting systems
- 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
- Certification of Termination Proofs Using CeTA
- Proving Termination Using Recursive Path Orders and SAT Solving
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Automated Termination Analysis for Logic Programs by Term Rewriting
- Proving Termination by Bounded Increase
- Certified Size-Change Termination
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Term Rewriting and All That
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Beyond Dependency Graphs
- Automated Termination Analysis of Java Bytecode by Term Rewriting
- Logic for Programming, Artificial Intelligence, and Reasoning
- Termination Analysis with Calling Context Graphs
- Termination of logic programs: Transformational methods revisited
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Proving termination by dependency pairs and inductive theorem proving
