Difference between revisions of "MicroTTT"
From Termination-Portal.org
Jump to navigationJump to search| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | MicroTTT | + | MicroTTT is a prototype written in OCaml that generates XML-output as termination proofs using only the dependency pair transformation, estimated dependency graphs, strongly connected components decomposition, and simple projections combined with the subterm criterion. Additionally it is possible to read in such XML-proofs and - using the same methods as for generating a proof - check them for correctness. |
| + | * the source code is available [http://cl-informatik.uibk.ac.at/~griff/mttt/mttt.tar.bz2 here] | ||
| + | * the specification of the XML-format [http://cl-informatik.uibk.ac.at/~griff/mttt/rscc.xsd here] | ||
| + | Note that Ruby needs to be installed for compilation of microTTT, since the internal preprocessor of it is written in that language. | ||
Latest revision as of 13:06, 21 May 2008
MicroTTT is a prototype written in OCaml that generates XML-output as termination proofs using only the dependency pair transformation, estimated dependency graphs, strongly connected components decomposition, and simple projections combined with the subterm criterion. Additionally it is possible to read in such XML-proofs and - using the same methods as for generating a proof - check them for correctness.
Note that Ruby needs to be installed for compilation of microTTT, since the internal preprocessor of it is written in that language.
