[Termtools] New release of Rainbow

[Frederic Blanqui]

Dear all,

I am quite happy to announce a new release of Rainbow, a termination
proof certification back-end based on CoLoR, a Coq Library on Rewriting
and termination, and Coq 8.2.

-------------------------------------------------------
TPDB termination problems supported by Rainbow
-------------------------------------------------------

- TRS standard
- TRS relative (->= rules)
- TRS modulo equations l=r with Var(l)=Var(r) (e.g. associativity
   and commutativity) are translated into TRS relative
- SRS standard
- SRS relative

-------------------------------------------------------
Proof techniques supported by Rainbow
-------------------------------------------------------

- dependency pair transformation (with or without marked symbols)
- dependency graph decomposition
- polynomial interpretation
- matrix interpretation (standard, arctic and below-zero)
- argument filtering (without projection)
- SRS reversal

The syntax of termination certificates is precisely described in
grammar/proof.xsd.

You can download CoLoR and Rainbow on the new CoLoR web page
http://color.inria.fr.

Best regards, Frederic.