[Termtools] Certified relative / equational termination

[Johannes Waldmann]

> Therefore I think it would be nice to have categories such as
> "TRS/SRS Relative Certifying" and "TRS Equational Certifying" 

(speaking as myself:)

I'm all for certification.

What exactly is "TRS Equational"?  Is that "modulo theories"?

Does not really matter since in fact, being certified (or not)
is *orthogonal* to the categories (of rewrite systems/programs),
that is, each of them could (should) be certified.

Besides, "complexity" is again orthogonal.
So we could have certified proofs
of innermost derivational complexity, etc.


(speaking as the committee chair:)

Please set up a page on termination-portal.org
with a concrete proposal (including examples if necessary).
Then we can discuss and decide (perhaps during WST)
how to integrate this into the competition/execution environment.


Best regards, Johannes.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20090424/f937e068/attachment.pgp