[isabelle] IsaFoR: a proof library on first order term rewriting



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.