The Coq mailing list

[Xavier Urbain <Xavier.Urbain AT lri.fr>]

Hi everyone,

We are making available a prototype dedicated to proving termination
of first order term rewriting systems with full automation. The tool
(CiME2.99beta) produces coq files that certify well-foundedness of
the relation described by the TRS, i.e. it proves (well_founded R). It
is based on the Coccinelle library developed by the A3PAT project.
http://www3.ensiie.fr/~urbain/a3pat

 Termination power includes several criteria, and allows the use of
different orderings in an involved proof. However, it does not use all
the techniques in CiME2.04 yet.

 Up to now it certifies terminating about 300 problems from the TPDB.

 Binary files for i686 as well as an example session are available
from the website of the project. Do not hesitate to ask for binaries
for your architecture.

 Feedback and requests are welcome!


 Cheers,

 Xavier

  --

Xavier Urbain
-----------------------------------------------------------------
CEDRIC, CPR

C.N.A.M. -- E.N.S.I.I.E.
-----------------------------------------------------------------