Cdiprover3: A Tool for Proving Derivational Complexities of Term Rewriting Systems.
Andreas Schnabl · 2009
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 com-plexity of the considered system. We explain the tool in detail, and give an overview of the employed proof methods. 1.