CORR
2006
Springer
13 years 11 months ago
2006
Springer
Abstract. This paper introduces a propositional encoding for lexicographic path orders in connection with dependency pairs. This facilitates the application of SAT solvers for term...
FROCOS
2007
Springer
14 years 5 months ago
2007
Springer
We introduce a propositional encoding of the recursive path order with status (RPO). RPO is a combination of a multiset path order and a lexicographic path order which considers pe...