PV1 $T_TT_2$: Tyrolean Termination Tool 2produces a proof of termination for a term rewrite system

Tyrolean Termination Tool 2 is a tool for automatically proving and disproving termination of rewrite systems.

Application domain/field

Type of tool

Termination analyzer

Expected input

Term rewrite system

Format:

TPDB format

Expected output

Whether the term rewrite system terminates or not (YES, NO, MAYBE) It also shows the following:

Internals

Uses MiniSat and Yices.

Comments

License: GNU LGPL V3.0?
Termination

Links

Last commit date

5 July 2021

Related papers

https://doi.org/10.1007/978-3-642-02348-4_21 (RTA '09)

Last publication date

2009

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.