[Termtools] LP category

[Peter Schneider-Kamp]

Dear all,

the LP category has finished and, as expected, it has been
a close call. In between, Polytool was 5 examples ahead of
AProVE, which in the end solved 8 more.

Congratulations to Polytool for being the first tool to
prove termination of the snake example (and its variante csnake):
http://colo5-c703.uibk.ac.at:8080/termcomp/tpdb/tpviewer.seam?tpId=6669&cid=3091

The competition run has also demonstrated, that further
discussion regarding the handling of undefined/built-in
predicates and non-logical operators is needed, cf.
http://termination-portal.org/wiki/Logic_Programming

Regards from Aachen,
Peter
-- 
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/psk
RWTH Aachen            phone: +49 241 80-21211