To be entered into ProoVer systems must be registered using the ProoVer system registration form by the registration deadline.

For each system entered an entrant must be nominated to handle all issues (e.g., installation and execution difficulties) arising before, during, and after the competition. The nominated entrant must formally register for ProoVer. It is not necessary for entrants to physically attend the competition (but funnier!).

Note that, if you participate to both CASC and ProoVer, you only have to pay the registration fees once!

System Description

A system description must be provided for each proof checker system, using this HTML schema. The schema has the following sections:

  • Overview: This section introduces the proof checker and its main design choices. It may also describe its checking strategy, including when the system reports “NotVerified” versus attempting additional verification steps, as well as any notable features.
  • Implementation: This section describes the implementation of the proof checker system, including the programming language used, important internal data structures, and any special code libraries. It should also specify any backend ATP or external tools used. The availability of the system is given here. A brief explanation of how proofs are verified should also be included.
  • Expected competition performance: This section makes some predictions about the performance of the proof checker.
  • References.

The system description must be emailed to the competition organizer by the system submission deadline. The system descriptions form part of the competition proceedings.

Sample Solutions

For systems in the divisions that require solution output, representative sample solutions must be emailed to the competition organizer by the sample solutions deadline. Sample must be run on the examples from the example page.