cl-banner

Increasing Interpretations

Harald Zankl and Aart Middeldorp

Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2008), Lecture Notes in Artificial Intelligence 5144, pp. 191 – 205, 2008.

Abstract

The paper at hand introduces a refinement of interpretation based termination criteria for term rewrite systems in the dependency pair setting. Traditional methods share the property that—in order to be successful—all rewrite rules must (weakly) decrease with respect to some measure. The novelty of our approach is that we allow some rules to increase the interpreted value. These rules are found by simultaneously searching for adequate polynomial interpretations while considering the information of the dependency graph. We prove that our method extends the termination proving power of linear natural interpretations. Furthermore, this generalization perfectly fits the recursive SCC decomposition algorithm which is implemented in virtually every termination prover dealing with term rewrite systems.

 

  PDF |    doi:10.1007/978-3-540-85110-3_16  |  © Springer

BibTeX 

@inproceedings{HZAM-AISC08,
author = "Harald Zankl and Aart Middeldorp",
title = "Increasing Interpretations",
booktitle = "Proceedings of the 9th International Conference on
Artificial Intelligence and Symbolic Computation",
series = "Lecture Notes in Artificial Intelligence",
volume = 5144,
pages = "191--205",
publisher = "Springer-Verlag",
year = 2008
}
Nach oben scrollen