cl-banner

Proofs of Termination of Rewrite Systems for Polytime Functions

Toshiyasu Arai and Georg Moser

Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005), Lecture Notes in Computer Science 3821, pp. 529 – 540, 2005.

Abstract

We define a new path order <pop so that for a finite rewrite system R compatible with <pop, the complexity or derivation length function DlRf for each function symbol f is guaranteed to be bounded by a polynomial in the length of the inputs. Our results yield a simplification and clarification of the results obtained by Beckmann and Weiermann (Archive for Mathematical Logic, 36:11–30, 1996).

 

  PDF |    doi:10.1007/11590156_43  |  © Springer

BibTeX 

@inproceedings{TAGM-FSTTCS05,
author = "Toshiyasu Arai and Georg Moser",
title = "Proofs of Termination of Rewrite Systems for Polytime Functions",
booktitle = "Proceedings of the 25th International Conference on
Foundations of Software Technology and Theoretical Computer Science",
series = "Lecture Notes in Computer Science",
volume = 3821,
pages = "529--540",
publisher = "Springer-Verlag",
year = 2005
}
Nach oben scrollen