| Predictive Labeling with Dependency Pairs using SAT |  |
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.
Predictive Labeling with Dependency Pairs using SAT
In
Proceedings of the 21st International Conference on Automated Deduction
( CADE '07),
Bremen, Germany.
BibTeX:@inproceedings{predlab-CADE-07,
author = {Adam Koprowski and Aart Middeldorp},
title = {Predictive Labeling with Dependency Pairs using {SAT}},
booktitle = {Proceedings of the 21st International Conference on Automated Deduction (CADE '07)},
year = {2007},
series = {Lecture Notes in Artificial Inteligence},
volume = {4603},
pages = {410--425},
} | 
