The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

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 Problem Data Base
TRS = Term Rewrite System
SRS = String Rewrite System

-------------------------------------------------------
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.

PS. The TPDB is available on 
http://colo5-c703.uibk.ac.at:8080/termcomp/home.seam. The site of the 
termination competition is 
http://termination-portal.org/wiki/Termination_Competition.