Solving Partial Order Constraints for LPO Termination
From MaRDI portal
Publication:3527280
DOI10.1007/11805618_2zbMATH Open1151.68631arXivcs/0512067OpenAlexW2171453216MaRDI QIDQ3527280FDOQ3527280
Authors: Michael Codish, V. Lagoon, Peter J. Stuckey 
Publication date: 25 September 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract: This paper introduces a new kind of propositional encoding for reasoning about partial orders. The symbols in an unspecified partial order are viewed as variables which take integer values and are interpreted as indices in the order. For a partial order statement on n symbols each index is represented in log2 n propositional variables and partial order constraints between symbols are modeled on the bit representations. We illustrate the application of our approach to determine LPO termination for term rewrite systems. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with current implementations for LPO termination. The proposed encoding is general and relevant to other applications which involve propositional reasoning about partial orders.
Full work available at URL: https://arxiv.org/abs/cs/0512067
Recommendations
- Solving partial order constraints for LPO termination
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Proving Termination Using Recursive Path Orders and SAT Solving
- SAT Solving for Argument Filterings
- Orderings and Constraints: Theory and Practice of Proving Termination
Cited In (10)
- Proving termination of context-sensitive rewriting with MU-TERM
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Decreasing diagrams and relative termination
- Decreasing diagrams and relative termination
- Argument filterings and usable rules for simply typed dependency pairs
- Transforming SAT into termination of rewriting
- KBO orientability
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Solving partial order constraints for LPO termination
- Proving Termination with (Boolean) Satisfaction
This page was built for publication: Solving Partial Order Constraints for LPO Termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3527280)
