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

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.

• Type: Journal
• Year: 2009
• Where: ESSLLI
• Authors: Andreas Schnabl
• Keywords: Automated Reasoning, Dependent Interpretations, ESSLLI 2009, Polynomial Interpretations, Small Bounds