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.

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
}