A SAT-based Implementation for RPO Termination

Elena 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


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

© copyright notice