Proving Termination Using Recursive Path Orders and SAT Solving
From MaRDI portal
Publication:3525016
DOI10.1007/978-3-540-74621-8_18zbMath1148.68393OpenAlexW1820313840MaRDI QIDQ3525016
René Thiemann, Michael Codish, Elena Annov, Peter Schneider-Kamp, Jürgen Giesl
Publication date: 16 September 2008
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-74621-8_18
Related Items (10)
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion ⋮ KBO orientability ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Automated Implicit Computational Complexity Analysis (System Description) ⋮ A SAT-Based Approach to Size Change Termination with Global Ranking Functions ⋮ Complexity Analysis by Rewriting ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ Argument Filterings and Usable Rules for Simply Typed Dependency Pairs ⋮ Proving Termination with (Boolean) Satisfaction
Uses Software
This page was built for publication: Proving Termination Using Recursive Path Orders and SAT Solving
