A SAT-based Implementation for RPO Termination
International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (Short Paper);
Abstract:This paper introduces a propositional encoding of the recursive path order (RPO) on terms which is a combination of a multiset path order and a lexicographic path order which considers permutations of the arguments in the lexicographic comparison. The proposed encoding allows us to use SAT solvers in order to determine whether a given term rewrite system is RPO terminating.
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel