SAT solving for termination proofs with recursive path orders and dependency pairs
From MaRDI portal
Publication:2392415
DOI10.1007/s10817-010-9211-0zbMath1276.68140OpenAlexW2081479337MaRDI QIDQ2392415
Peter Schneider-Kamp, Michael Codish, Jürgen Giesl, 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
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)
Related Items
Analyzing program termination and complexity automatically with \textsf{AProVE}, Harnessing First Order Termination Provers Using Higher Order Dependency Pairs, Size-based termination of higher-order rewriting, AC-KBO revisited, A Lambda-Free Higher-Order Recursive Path Order
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Termination of rewriting systems by polynomial interpretations and its implementation
- Orderings for term-rewriting systems
- Implementing logical connectives in constraint programming
- Compiling finite linear CSP into SAT
- KBO orientability
- Tyrolean termination tool: techniques and features
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Increasing interpretations
- On recursive path ordering
- Termination of term rewriting using dependency pairs
- Automating the dependency pair method
- SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
- Maximal Termination
- Proving Termination Using Recursive Path Orders and SAT Solving
- Predictive Labeling with Dependency Pairs Using SAT
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Term Rewriting and All That
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- SAT Solving for Argument Filterings
- Constraints for Argument Filterings
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Frontiers of Combining Systems
- Search Techniques for Rational Polynomial Orders
- Logic for Programming, Artificial Intelligence, and Reasoning
