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

Term rewriting
Termination
Term rewrite system (TRSs)

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:

Term rewrite system/problem
Proof of termination
Time it took to find the proof

Internals

Uses MiniSat and Yices.

Comments

Also spellt as

T_{T} T_{2}

. License: GNU LGPL V3.0?

Termination

Related papers

Tyrolean Termination Tool 2 (RTA '09)

Last publication date

2009

Related tools

Successor of $T_{T} T$
Other automated termination analyzers: AProVE, JamBox
$T_{T} T_{2}$ is used by the following tools: CaT, ConCon, KBCV, mkbTT, TcT, Wanda

ProVerB specific

Markdown description: view/edit
Reason for this entry: compared to nonreach
Contained in the ProVerB22 dataset (paper + artefact)

Program
Verification
Book

PV1 ⊧ TTT2: Tyrolean Termination Tool 2produces a proof of termination for a term rewrite system

Application domain/field

Type of tool

Expected input

Expected output

Internals

Comments

Links

Related papers

Last publication date

Related tools

ProVerB specific

ProgramVerificationBook

PV1 ⊧ TTT2: Tyrolean Termination Tool 2produces a proof of termination for a term rewrite system

Application domain/field

Type of tool

Expected input

Expected output

Internals

Comments

Links

Related papers

Last publication date

Related tools

ProVerB specific

Program
Verification
Book