Proving Termination Using Recursive Path Orders and SAT Solving

DOI10.1007/978-3-540-74621-8_18MaRDI QIDQ3525016zbMATH OpenOpenAlexFDO

Authors Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish, 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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• SAT solving for termination proofs with recursive path orders and dependency pairs
• scientific article; zbMATH DE number 3905845
• Proving Termination with (Boolean) Satisfaction
• Orderings and Constraints: Theory and Practice of Proving Termination
• Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
• scientific article; zbMATH DE number 408817
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• A path ordering for proving termination of AC rewrite systems
• A methodology for proving termination of logic programs

Cited in

(19)

• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• SAT solving for termination proofs with recursive path orders and dependency pairs
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Encoding dependency pair techniques and control strategies for maximal completion
• Solving Partial Order Constraints for LPO Termination
• Automated Implicit Computational Complexity Analysis (System Description)
• Solving partial order constraints for LPO termination
• Argument filterings and usable rules for simply typed dependency pairs
• Proving termination by dependency pairs and inductive theorem proving
• Transforming SAT into termination of rewriting
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• SAT Solving for Argument Filterings
• A SAT-Based Approach to Size Change Termination with Global Ranking Functions
• Complexity Analysis by Rewriting
• Proving Termination with (Boolean) Satisfaction
• Correspondence between composite theories and distributive laws
• Certifying the weighted path order (invited talk)
• Inferring RPO symbol orderings
• KBO orientability

Describes a project that uses

Uses Software

• Tyrolean
• MiniSat

This page was built for publication: Proving Termination Using Recursive Path Orders and SAT Solving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3525016)