cl-banner

Cdiprover3: A Tool for Proving Derivational Complexities of Term Rewriting Systems

Andreas Schnabl

Interfaces: Explorations in Logic, Language and Computation, Lecture Notes in Artificial Intelligence 6211, pp. 142 – 154, 2010.

Abstract

This paper describes cdiprover3, a tool for proving termination of term rewrite systems by polynomial interpretations and context dependent interpretations. The methods used by cdiprover3 induce small bounds on the derivational complexity of the considered system. We explain the tool in detail, and give an overview of the employed proof methods.

 

  PDF |    doi:10.1007/978-3-642-14729-6_11  |  © Springer

BibTeX 

@inproceedings{AS-ESSLLI08,
author = "Andreas Schnabl",
title = "Cdiprover3: A Tool for Proving Derivational Complexities of Term Rewriting Systems",
booktitle = "Interfaces: Explorations in Logic, Language and Computation",
series = "Lecture Notes in Artificial Intelligence",
volume = 6211,
pages = "142--154",
publisher = "Springer-Verlag",
year = 2010
}
Nach oben scrollen