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

zbMATH Keywords

term rewritingSAT solvingterminationdependency pairsrecursive path order

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)

Recommendations

• Proving Termination Using Recursive Path Orders and SAT Solving
• SAT Solving for Argument Filterings
• Solving partial order constraints for LPO termination
• Solving Partial Order Constraints for LPO Termination
• SAT Solving for Termination Analysis with Polynomial Interpretations

Cites Work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• A SAT-Based Approach to Size Change Termination with Global Ranking Functions
• Automating the dependency pair method
• Compiling finite linear CSP into SAT
• Constraints for Argument Filterings
• Frontiers of Combining Systems
• Implementing logical connectives in constraint programming
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Increasing interpretations
• KBO orientability
• Logic for Programming, Artificial Intelligence, and Reasoning
• Matrix interpretations for proving termination of term rewriting
• Maximal Termination
• Mechanizing and improving dependency pairs
• On recursive path ordering
• Orderings for term-rewriting systems
• Predictive Labeling with Dependency Pairs Using SAT
• Proving Termination Using Recursive Path Orders and SAT Solving
• SAT Solving for Argument Filterings
• SAT Solving for Termination Analysis with Polynomial Interpretations
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
• Search Techniques for Rational Polynomial Orders
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Solving partial order constraints for LPO termination
• Term Rewriting and All That
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination of term rewriting using dependency pairs
• Tyrolean termination tool: techniques and features

Cited In (13)

• 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
• Transforming SAT into termination of 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
• Comparing CSP and SAT solvers for polynomial constraints in termination provers
• Proving Termination Using Recursive Path Orders and SAT Solving
• Solving Partial Order Constraints for LPO Termination

Uses Software

• MiniSat
• Sat4j
• Tyrolean
• AProVE
• PrecoSAT
• Glucose
• Sugar
• TCAS
• REVE

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)