SAT Techniques for Lexicographic Path Orders
Harald Zankl · arXiv (Cornell University) · 2006
This seminar report is concerned with expressing LPO-termination of term rewrite systems as a satisfiability problem in propositional logic. After relevant algorithms are explained, experimental results are reported.