Solving Partial Order Constraints for LPO Termination
Michael Codish, Vitaly Lagoon, Peter J. Stuckey · Journal on Satisfiability Boolean Modeling and Computation · 2008
This paper introduces a propositional encoding for lexicographic path orders (LPOs) and the corresponding LPO termination property of term rewrite systems. Given this encoding, termination analysis can be performed using a state-of-the-art Boolean sa