[Termtools] termination competition changes
Lars Noschinski
lars.noschinski at rwth-aachen.de
Sun Feb 22 23:58:29 CET 2009
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
More information about the Termtools
mailing list