Description

TTTbox is an automated termination prover for rewrite systems. It provides an implementation of the match-bound technique for string and term rewrite systems described in papers by Geser, Hofbauer, Waldmann and Zantema. In addition, TTTbox can be also used to prove termination of non-left-linear term rewrite systems via the match-bound technique. A previous version of TTTbox took part at the international Termination Competition 2006.

Implementation

TTTbox is written in OCaml an consists of about 5000 lines of code. About 64% is used to implement the match-bound technique. The rest is used to deal with input (about 11%) and to produce output (about 25%).

Downloads

To download the latest version of TTTbox, click on the following link: tttbox.zip

Usage

The command ./tttbox [options] <TRS/SRS filename> [timeout] executes TTTbox. The TRS/SRS file format correspond to the WST file format. The measure of timeout are seconds. The following options can be used to control TTTbox:

-help	explanation of TTTbox
-rfc	construct right-hand sides of forward closures
-ruf	remove rewrite rules which contain a function symbol that does not occur in any right-hand side
-complex	use implicit algorithm to close tree automata under raise-rules
-naive	use explicit algorithm to close tree automata under raise-rules
-automaton	show the compatible tree automaton in the proof
-text	produce text output
-name <text>	name of the output file (without extension)

Experiments

To get more detailed information on the experiments done with TTTbox, choose the appropriate paper from the publication list and click on Experiments.

Contact

For any question related to TTTbox do not hesitate to contact me via the e-mail address martin.korp__AT__uibk.ac.at.