[Termtools] CeTA: a stand-alone termination proof certifier

[René Thiemann]

Dear all,

we are happy to announce IsaFoR and CeTA which are both freely
available at:

   http://cl-informatik.uibk.ac.at/software/ceta/

* IsaFoR (Isabelle Formalization of Rewriting) is an Isabelle/HOL
   library which formalizes first order term rewriting.
   It currently contains several definitions, theorems, and
   algorithms about rewriting, where the main focus is on
   termination analysis.

   - terms, TRSs, matching, unification
   - dependency pairs (incl. dependency pair framework)
   - dependency graph processor (EDG***, i.e., EDG* with tcap)
   - reduction pair processor
   - polynomial orders
   - nontermination via loops
   - ...

   For each of the termination techniques, IsaFoR contains a check- 
function
   which--given a termination proof from an arbitrary termination
   prover--checks whether these techniques have been applied in a  
correct
   way. Hence, these functions can be used to certify termination proof
   trees.

* Since all our check-functions are executable, we used Isabelle's
   code-generation facilities to generate a certified Haskell program,
   CeTA (Certified Termination Analysis), which can then also be used
   to certify termination proof trees. It has the following benefits:

   - readable error messages in case a proof tree is refuted
   - execution time: certification of over 500 proofs in 1 minute
   - robustness: any dependency graph estimation is accepted,
                 as long as it is subsumed by EDG***
   - modularity: for each termination technique one can call an  
individual
	        check-function, the whole proof tree is not required
   - easy usage: just download a binary or some Haskell-files,
                 an installation of Isabelle is not required;
                 simple proof tree format

* For the future we have the following plans:
   - subterm criterion
   - negative polynomial orders
   - combination with other termination proof certifiers via common
     XML proof tree format (we aim for some results after WST'09)
   - submission to the archive of formal proofs
   - ...

So stay tuned.

Best regards,
Christian Sternagel,
René Thiemann, and
Harald Zankl