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

[Claude Marche]

I have no precise answer for this question, in the sense that I cannot
provide a description of the language of proof traces. But the goal is
to go into this direction.

Nevertheless, there is a general answer : a proof trace is some
description that would allow to systematically check the termination
of the given problem. In other words, although the problem "is P
terminating ?" undecidable in general, the problem "is T a valid trace
for the termination of P ?" should be decidable.

So, in the case your tool proves termination using the RFC match
bound, you should provide :

1) the exact criterion used: a bibtex reference, or an URL, to the
   exact theoretical result.
2) additional needed information, such as the value of the bound

but you need not display the automaton, since as far as I understand
match bound criterion, anybody can compute the automaton from the SRS
and the chosen bound.

Let's imagine you prove termination of a TRS using the classical
Manna-Ness criterion and a MPO, then you need to say

1) that you use Manna-Ness criterion (\cite{...})
2) with the reduction ordering MPO (\cite{...}) with
     precedence ......

I hope you get the idea. Again, the key is simply that there is enough
information for the termination being double-checked systematically.

- Claude

>>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:

    Johannes> 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. 

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

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

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

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

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

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

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


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

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools