|
A SAT-based Implementation for RPO TerminationElena Annov, Michael Codish, Jürgen Giesl, Peter Schneider-Kamp and René Thiemann
International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (Short Paper);
2006
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.Available: bibtex entry pdf Michael Codish The Department of Computer Science Ben-Gurion University of the Negev PoB 653, Beer-Sheva, 84105, Israel mcodish@cs.bgu.ac.il
|