[Termtools] competition - (preliminary) results

[Rene Thiemann]

Hi,

> > Perhaps the authors could comment on the difference between the provers?
> > What would be the "combined" score (i. e. if Aprove had Matrices,
> > or if Jambox had ... what exactly? Size change principle perhaps)?
>
> If I have counted correctly then the combined score should be 669.
>
> I think most of the systems that AProVE is able to solve, but Jambox
> fails, are due to Narrowing. Can you confirm this?

This is correct for termination proofs. Most of the examples we can prove 
terminating where Jambox fails, are due to DP-transformations (narrowing, 
(forward)-instantiation, and rewriting). However, for some reason Jambox only 
disproved termination of SRSs in the competition. There Matchbox is much 
closer. But for disproving we did not yet investigate why we can handle 16 % 
more examples than Matchbox.

Best regards,
Rene
-- 
René Thiemann         mailto:thiemann at informatik.rwth-aachen.de
LuFG Informatik II    http://www-i2.informatik.rwth-aachen.de/thiemann
RWTH Aachen           phone: +49 241 80-21241

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools