PV1 TTT2: 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

Also spellt as TTT2. License: GNU LGPL V3.0?
Termination

Links

Related papers

Tyrolean Termination Tool 2 (RTA '09)

Last publication date

2009

Related tools

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.