[Termtools] termination competition changes

[Lars Noschinski]

Hello,

* Aart Middeldorp <Aart.Middeldorp at uibk.ac.at> [09-02-13 20:53]:
> http://termination-portal.org/wiki/XTC_Format_Specification

In Aachen, we are currently working on TRS with predefined rules for
integers. As there are infinitely many predefined rules ( like 1 + 1 ->
2, 1 + 2 -> 3, ...), those cannot be expressed with the proposed format.
Apart from the infinite number of rules, those are normal TRS (with the
additional restriction, that occurence of predefined symbols on the lhs
is limited).

As we would like to submit this as a new format to the competition in
the not-too-distant future, I'd like the XTC format to be able to
express such TRS.

My suggestion would be to add a new (optional) element which may
occur directly under problem which contains a (list of?) strings
referring to some predefined semantics.

So a definition of an integer TRS could look like this:

<problem>
    <predefined>integers</predefined>
    [...]
</problem>

Upon encountering the "predefined" element, a prover knows, that
either

    it is unable to handle this problem, as it does not know how to
    handle "integers"

or

    there are additional function symbols like 1, 2, 3, ..., +, -, ...,
    with a certain set of predefined rules and some restrictions on the
    function symbols on the lhs.


 - Lars Noschinski