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

[Frederic Blanqui]

Congratulations! It is a very good idea to use an extracted program. It 
allows you to get round the slowness of proof assistants. We did not do 
that with Rainbow and CoLoR yet but it should not be too difficult to do 
it (Coq also has this feature). I will try to do that soon too ;-) Best 
regards, Frederic.

René Thiemann a écrit :
> 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
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools