SAT solving for termination proofs with recursive path orders and dependency pairs
DOI10.1007/S10817-010-9211-0zbMATH Open1276.68140OpenAlexW2081479337MaRDI QIDQ2392415FDOQ2392415
Authors: Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann 
Publication date: 1 August 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9211-0
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)
Cites Work
- Termination of rewriting systems by polynomial interpretations and its implementation
- Termination of term rewriting using dependency pairs
- Orderings for term-rewriting systems
- SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
- Term Rewriting and All That
- Title not available (Why is that?)
- Automating the dependency pair method
- Title not available (Why is that?)
- Frontiers of Combining Systems
- Logic for Programming, Artificial Intelligence, and Reasoning
- Tyrolean termination tool: techniques and features
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Proving Termination Using Recursive Path Orders and SAT Solving
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Search Techniques for Rational Polynomial Orders
- KBO orientability
- Implementing logical connectives in constraint programming
- Compiling finite linear CSP into SAT
- On recursive path ordering
- Maximal Termination
- Predictive Labeling with Dependency Pairs Using SAT
- SAT Solving for Argument Filterings
- Constraints for Argument Filterings
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Increasing interpretations
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Solving partial order constraints for LPO termination
Cited In (11)
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- SAT Solving for Argument Filterings
- Harnessing first order termination provers using higher order dependency pairs
- Size-based termination of higher-order rewriting
- AC-KBO revisited
- Solving partial order constraints for LPO termination
- Predictive Labeling with Dependency Pairs Using SAT
- A Lambda-Free Higher-Order Recursive Path Order
- Proving Termination with (Boolean) Satisfaction
- Proving Termination Using Recursive Path Orders and SAT Solving
- Solving Partial Order Constraints for LPO Termination
Uses Software
This page was built for publication: SAT solving for termination proofs with recursive path orders and dependency pairs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2392415)
