[Termtools] (sub) categories, specification of input format, test cases

[Peter Schneider-Kamp]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Johannes Waldmann wrote:
> how many unsolved problems from the first round (1 minute)
> will be solved in the extension round (5 minutes) etc.)

Very few would be my guess :) Maybe 10 in the standard TRS category.
There are not that many examples that last year's tools could not
prove in 60 seconds in the first place. I guess Matrix orderings
will decrease that pool even further. Also, for some of these
examples termination is unlikely to be proven automatically
(e.g, syracuse).

> But now, seriously.
> 
> The rules define the concept of "category" (SRS, TRS, LP)
> but not "sub-category" (as seen in last year's results table).
> 
> A prover must register for a (full) category,
> so it must behave correctly
> on all combinations of THEORY, STRATEGY,
> and relative and conditional rules, right?
> 
> That means if a prover decides to say "DONT KNOW"
> for relative termination problems, then it will loose some points
> (in the total score) with respect  to another prover
> that emits at least some proofs (e. g. by treating "->=" as "->")

I hope that the rules will be adapted/interpreted in the
spirit of last year's competition. That said, we should definitely
discuss and clarify the rules before the competition.

> And what are the implications for submitting secret problems?
> Each prover (author) submits up to 10 problems per category
> (irregardless of subcategory)?

That is a good question, too. I would prefer something like 5
per sub-category instead of 10 per category.

> The input format http://www.lri.fr/~marche/tpdb/format.html
> is semantically underspecified in several places, e. g.
> what happens for "(STRATEGY INNERMOST) (STRATEGY OUTERMOST) ..."
> what theories are pre-defined (A, C, AC  I guess)?
> what is "(THEORY (A x) (C x))", do these declarations accumulate?

What is "(THEORY (A f)) (STRATEGY INNERMOST)"? What is
"(THEORY (A f)) (STRATEGY CONTEXTSENSITIVE)"?

Kind regards,
Peter
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2.2 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFEfYfP3VbrCXkKHhwRAsAZAJ4hG3JLScUVIEvf0Jmeyuptlpea+gCePN7S
zQo0Z1EEetF9EnmVrgrSO5c=
=VE4T
-----END PGP SIGNATURE-----

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools