SAT Techniques for Lexicographic Path Orders
  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. 
Harald Zankl