[Termtools] [Termcomp] Fwd: Re: [color] Termination Competition 2009: Call for Participation

[Johannes Waldmann]

> Another question: if we provide a "checkme" command, what can be the 
> arguments? Is it possible to take as argument both the problem file and 
> the proof file as follows:
> 
> checkme xtc_file cpf_file?

As I understand, that would be redundant.
The proof contains the problem.
http://cl-informatik.uibk.ac.at/software/cpf/
root element: certificationProblem, child elements: input, proof


BTW, what has happened to the names:
XTC meant "xml format for Termination Certificates" (at WScT08)?
Now XTC denotes the input format only?

Is there any synchronisation between XTC and CPF?
It seems that XTC:trs (what version?)
is copied into CPF:trs but they are not identical
(e.g., signature and relrules are missing from CPF:trs?)
In fact CPF should just refer to XTC here?


Oh, and while we're at it - I think a naming like
"z001.xml" (as in current tpdb)  is wrong - it should be "z001.xtc"

Compare the naming conventions for source codes:
you don't say "quicksort.text" but "quicksort.java" (etc.)
because you then see that you need a Java compiler.
text (or xml) just denotes the visual represenation.


Best - Johannes.

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