[Termtools] naming, placing and contents of benchmarks (srs/cycles)

[Akihisa Yamada]

Dear Johannes and all,

> Wenzel's SRS and Cycle benchmarks should be added to TPDB,

Yes I will, but

> (but original name  should be kept as attribute,
> for later reference to results of this year's competition)

later reference will be anyway tedious if you rename benchmarks, as
anyone who wants to experimentally evaluate their method has to parse
XML only for comparing with previous TermComp results. So I'd rather
vote for keeping the names.

> We could make a separate directory
> for cycle termination problems.

I agree. Will it be called "Cycle_Rewriting"? Another option would be
"SRS_Graph" (foreseeing "TRS_Graph").

> We could also (additionally) put some annotation
> in the problems themselves.

In my opinion, an ideal solution is something like what ConCon has,
where filenames are just numbers and every information is given as a
tag (which can be used as a filter key). But it might be too much work
yet to implement this for TPDB.

Best regards,
Akihisa

> I think this annotation should be a "theory",
> because it is rewriting modulo conjugation (rotation).
>
> Note this cannot be expressed in the benchmark (XTC) format
> (where "theory" is attached to function symbol).
> Also, there is no "theory" (per se) in the CPF input tag
> (it has "acRewriteSystem").
>
> For historical reference, the original (plain text) format
> would be easier to extend for this,
> since it had THEORY declaration at the top level,
> https://www.lri.fr/~marche/tpdb/format.html
>
> - J.
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>

-- 
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/