[Termtools] Automation

[Xavier Urbain]

Hi everyone,

We are making available a prototype dedicated to proving termination
of first order term rewriting systems with full automation. The tool
(cime2.99alpha) 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. It does not use all the
techniques in CiME2 yet.

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

 A web page with binary files and example sessions will be set up in a
few days. Until then, 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.
-----------------------------------------------------------------