[Termtools] competition - (preliminary) results

[Jörg Endrullis]

Johannes Waldmann wrote:
> 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?

I have a experimental implementation of the size change principle with
embedding ordering. It would have given 2 or 3 extra points (but I
turned it off for the competition due to possible implementation bugs -
no time to test it).

The other way around matrix interpretations enable Jambox to solve some
systems where AProVE fails.

Best regards,
Jörg Endrullis
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools