Sciweavers

FROCOS
2007
Springer
13 years 11 months ago
Proving Termination Using Recursive Path Orders and SAT Solving
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...
Peter Schneider-Kamp, René Thiemann, Elena ...