[Termtools] termination competition bylaws

[Martin Johann Korp]

Dear community,

Due to a misconfiguration, TTT2 used an unsound strategy in the
SRS Relative and TRS Relative categories (the rfc extension of
match-bounds is not sound for relative rewriting and resulted in
yes/no conflicts).

Similar things happened to other tools (also in earlier years) and
there has been no uniform treatment (tools have been marked, removed,
got assigned penalty points). Hence we would like to push the
installation of bylaws and propose some possible formulations.
Clearly, the steering committee (in consultation with the host)
has to decide upon this.

[First unsoundness, etc. must be defined, not exclusive]

(u) A tool is unsound if one of its proofs contains a wrong deduction step.
(v) A tool is unsound if it gives a wrong answer (the answer is the
     first line of the output).
(w) Unsoundness of a tool is determined per category.

[We list the following statements as proposals, they are not exclusive]

(a) If a tool is unsound then it is removed from the corresponding category.
(b) If a tool is unsound then it is marked as buggy in the
     corresponding category.
(c) If a tool is unsound then a fixed version of it can be submitted and
     is rerun for the corresponding category. It is only allowed to fix the
     bug in the tool while no new features may be implemented.
     (c1) The results for the unsound tool stay in the table.
     (c2) The results for the unsound tool are removed from the table.
(d) If a tool is unsound, for each wrong answer a penalty is enforced,
     e.g., -8 points penalty for every wrong answer.
     (d1) The penalty is the same for all categories, although the scoring
          in the categories may be different.
     (d2) Each category selects its own penalty.
     (d3) There is a maximal number of wrong answers allowed (for example 3)
          and if a tool gives more than 3 wrong answers it is disqualified.
(e) The tool's authors can select one of (a)-(d).

Remarks:
   Option (d) is hard to check/implement since it cannot be done automatically.
   Option (d3) needs to define disqualification, e.g., remove tool from
category.
   Option (e) does not induce a uniform treatment.
   The -8 points penalty was suggested by Albert in an SC email on 22.12.2009.

Cheers, the TCT and TTT2 teams.