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

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
}