cl-banner

Constraints for Argument Filterings

Harald Zankl, Nao Hirokawa, and Aart Middeldorp

Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2007), Lecture Notes in Computer Science 4362, pp. 579 – 590, 2007.

Abstract

The dependency pair method is a powerful method for automatically proving termination of rewrite systems. When used with traditional simplification orders like LPO and KBO, argument filterings play a key role. In this paper we propose an encoding of argument filterings in propositional logic. By incorporating propositional encodings of simplification orders, the search for suitable argument filterings is turned into a satisfiability problem. Preliminary experimental results show that our logic-based approach is significantly faster than existing implementations.

 

  PDF |    doi:10.1007/978-3-540-69507-3_50  |  © Springer

BibTeX 

@inproceedings{ZHM-SOFSEM07,
author = "Harald Zankl and Nao Hirokawa and Aart Middeldorp",
title = "Constraints for Argument Filterings",
booktitle = "Proceedings of the 33rd International Conference on
Current Trends in Theory and Practice of Computer Science",
series = "Lecture Notes in Computer Science",
volume = "4362",
pages = "579--590",
publisher = "Springer-Verlag",
year = 2007
}
Nach oben scrollen