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

[René Thiemann]

Dear all,

> Johannes Waldmann a écrit :
>>> 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
> 
> It is redundant if the proof really contains the same problem...

since the CPF files should be usable stand-alone, one would not need the xtc-file. 
Nevertheless, it should be easily possible to pass both files to a certifier.

To circumvent that the input from the CPF file differs from the XTC-file there
are two scripts (available from the CPF-website) that automatically check whether
these TRSs coincide. It is planned that these scripts will be used for the competition.

>> 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?
> 
> I agree. This also means that giving the problem as argument is not completely redundant currently...

The signature in CPF is currently implicit as in the old TPDB format. As far as I remember there are
two reasons for this. First, signature declarations from theories like "f is AC" are now handled in a 
more flexible way by explicitly giving the equations. And second, the only other demand for termination
proofs are context-sensitive annotations. As there was no request for this feature yet, the signature
has not been added (yet).

However, relative rules can be expressed in CPF, cf. the <input> description. 

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

I see the point. However, one might take into account that the .xml extension has 
the advantage that browsers will directly apply the specified xsl-style-sheets 
for pretty-printing. 

Best regards,
René