Abstract

We present a general approach to encode termination in the dependency pair framework as a satisfiability problem, and include encodings of dependency graph and reduction pair processors. We use our encodings to increase the power of the completion tool Maxcomp.

BibTeX

@inproceedings{HSSW-WST14,
  author    = "Haruhiko Sato and Sarah Winkler",
  title     = "A Satisfiability Encoding of Dependency Pair Techniques for
               Maximal Completion",
  booktitle = "Proceedings of the 14th International Workshop on
               Termination",
  editor    = "Carsten Fuhs",
  pages     = "80--84",
  year      = 2014
}