CaT (Complexity AND Termination)

General Information

CaT is a powerful analyzer for the complexity of term rewrite systems. It is based on the fast and powerful termination analyzer TTT2. Among others, CaT won the category of derivational complexity in 2008, 2009, 2010, 2011, 2012, and 2013 in the international termination competition.


The current version is 1.5. Get recent versions.


Download and extract the archive. Look for a README file or contact one of the authors.

Contact Details

The main developers of CaT are Martin Korp and Harald Zankl. For questions do not hesitate to contact us.
Further contributors are Friedrich Neurauter and Christian Sternagel.