[Termtools] CoLoR: new release
Frederic Blanqui
frederic.blanqui at inria.fr
Mon Dec 7 09:09:46 CET 2009
Hello!
On http://color.inria.fr, you will find a new release of CoLoR, a Coq
Library on Rewriting and termination.
Among the main new features since the last release on March 11, you will
find:
- the use of N. Dershowitz's improvement for computing dependency pairs,
- the basic flat context closure transformation,
- a formalization of semantic labelling with models or quasi-models, and
infinite or finite sets of rules,
- root labelling, a particular case of semantic labelling,
- collapsing argument filterings (non-collapsing argument filterings
were already formalized),
- a loop checker for (relative) TRSs or SRSs,
- non-termination when the variable condition is not satisfied,
- the conversion into SRSs of TRSs with unary symbols only,
- signature morphisms and their properties wrt termination,
- semi-rings, matrices and matrix interpretations now operate on setoids,
- a syntactic matching algorithm proved correct and complete,
- positions in a term,
- the list of reducts of a term,
- a translation of CoLoR terms into Coccinelle terms
(http://a3pat.ensiie.fr/).
You can browse the definitions and lemmas on
http://color.inria.fr/doc/main.html.
Enjoy!
More information about the Termtools
mailing list