CASC-30

[Geoff Sutcliffe]

Hi ATP system developers, users, and supporters,

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, ATP systems - the world championship for such systems. One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems. Additionally, CASC aims to stimulate ATP research, motivate development and implementation of robust ATP systems that can be easily and usefully deployed in applications, provide an inspiring environment for personal interaction between ATP researchers, and expose ATP systems within and beyond the ATP community. CASC evaluates the performance of ATP systems in terms of the number of problems solved with an acceptable solution output, and the average time taken for problems solved, in the context of a bounded number of eligible problems and specified time limits.

CASC is held at each CADE and IJCAR conference - the major forums for the presentation of new research in all aspects of automated deduction. CASC-30 will be held  during the 30th International Conference on Automated Deduction (CADE-30).The CASC-30 web site ...
    https://tptp.org/CASC/30/
... contains lots more information. For those who intend to enter the competition, it includes the competition design, for you to read COMPLETELY and CAREFULLY ...
    https://tptp.org/CASC/30/Design.html
You'll see that there are now stronger requirements for proof output,
including use of TPTP4X to check syntax and GDV to check structure. I'll
be adding details over the coming days, but you can already use these
tools in SystemB4TPTP ...
    https://tptp.org/cgi-bin/SystemB4TPTP

Please do your system registration early ...
    https://tptp.org/CASC/30/SystemRegistration.html
It helps me keep things running smoothly without last minute chaos.

See you in Stuttgart!

Cheers,

Geoff

[Oscar Contreras]

Hi Geoff,

A question about EPR division: for the case of non-theorems is it necessary to include an SZS output section in addition to SZS status? If so, is a list of the set of saturated clauses enough?

Thanks in advance and cheers,

Oscar Contreras

--
You received this message because you are subscribed to the Google Groups "TPTP World" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tptp-world+...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tptp-world/196ddf96-4516-46b2-b1bb-4c71bee8e038n%40googlegroups.com.