[Fwd: how much detail in proofs (esp. RFC match bounds) - was: Re: [Termtools] Next competition]

[Johannes Waldmann]

Claude Marche wrote:

>    output will be expected to have the form 
>  
>    first line : YES or NO
>    remaining : a proof trace in english, with reference to criteria
>    involved. 

of course I agree. But can you be a bit more specific.
What is a "reference"? Do you want the bibtex entry :-)
or just some string (e. g. "RFC match bound")
that would yield the right thing when google-d?

looking at last year's competition, what proofs are there
where you would expect more detail? (Of course this is a question
not just to Claude, but to anyone involved in the competition.)

E. g. for match-bound proofs, do you want to see the complete automaton?
These things can get large (thousands of states), see
http://www.lri.fr/%7Emarche/termination-competition/2005/webform.cgi?command=viewres&tool=jambox&prob=secret2005.jambox3.srs

If you say that you have enough space,
then I think we could easily emit the automata
(although that would increase our running times a bit)

Keeping in mind the goal of automated verification,
of course it would be good to have a common automaton format
that all tools (*box, Torpa, Aprove) could use.
At the very least, it would have to contain information on:
* which symbol is the right-end marker
* which states are initial/final
* the transition relation, as a set of tuples
  ( state, symbol, height, state ) for normal transitions
  and ( state, state ) for epsilon transitions (important for Jambox)
for completeness, it should also contain the signature
and the state set although these could be inferred.

(I suggest to discuss this match-bound specific stuff here on the list
but with a clearly marked "RFC-mb" or similar in the subject line.
Claude - did you solve the archive accessibility problem?)

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------


_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools