Predictive Labeling with Dependency Pairs using SAT

Adam Koprowski and Aart Middeldorp

Proceedings of the 21st International Conference on Automated Deduction (CADE 2007), Lecture Notes in Artificial Intelligence 4603, pp. 410 – 425, 2007.


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.


  PDF |    doi:10.1007/978-3-540-73595-3_31 |  © Springer


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
Nach oben scrollen