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

[Juergen Giesl]

Dear all,


> 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 "->")

Here, my proposal would be that each prover should be
allowed to specify the sub-categories that it works on.
Then a prover for "TRS" can specify that it doesn't work
for relative termination problems. I also think it makes more
sense to count points separately for the separate sub-categories.
(This proposal is just what was done in the last competition.)

Best Regards
Juergen



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