Proving Termination with (Boolean) Satisfaction
From MaRDI portal
Publication:5504589
DOI10.1007/978-3-540-78769-3_1zbMATH Open1179.68034OpenAlexW2177928386MaRDI QIDQ5504589FDOQ5504589
Authors: Michael Codish 
Publication date: 22 January 2009
Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-78769-3_1
Recommendations
- SAT solving for termination proofs with recursive path orders and dependency pairs
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- SAT-based termination analysis using monotonicity constraints over the integers
- SAT Solving for Termination Analysis with Polynomial Interpretations
- SAT Solving for Argument Filterings
Cites Work
- Termination of term rewriting using dependency pairs
- The size-change principle for program termination
- Orderings for term-rewriting systems
- A machine program for theorem-proving
- Termination of rewriting
- Logic programming with satisfiability
- Proving Termination Using Recursive Path Orders and SAT Solving
- Solving Partial Order Constraints for LPO Termination
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Term Rewriting and Applications
- On recursive path ordering
- Termination of String Rewriting with Matrix Interpretations
- SAT Solving for Argument Filterings
- Satisfying KBO Constraints
- Matrix Interpretations for Proving Termination of Term Rewriting
- Computer Aided Verification
- Programming Languages and Systems
Cited In (3)
Uses Software
This page was built for publication: Proving Termination with (Boolean) Satisfaction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5504589)
