Abstract

This paper combines predictive labeling with dependency pairs and
reports on its implementation. Our starting point is the method of
proving termination of rewrite systems using semantic labeling
with infinite models in combination with lexicographic path
orders. We replace semantic labeling with predictive labeling to
weaken the quasi-model constraints and we combine it with
dependency pairs (usable rules and argument filtering) to increase
the power of the method. Encoding the resulting search problem as
a propositional satisfiability problem and calling a
state-of-the-art SAT solver yields a powerful technique for
proving termination automatically.

BibTeX

@inproceedings{KM-CADE07,
  author      = "Adam Koprowski and Aart Middeldorp",
  title       = "Predictive Labeling with Dependency Pairs using {SAT}",
  booktitle   = "Proceedings of the 21st International Conference on
                 Automated Deduction",
  series      = "Lecture Notes in Artificial Intelligence",
  publisher   = "Springer-Verlag",
  volume      = 4603,
  pages       = "410--425",
  year        = 2007
}