Systems, Problems, and Ranking

Systems

• Classical 1st order logic and now Typed higher-order logic
• Soundness required
• Theoretical and implementation completeness not required
• Fully automatic
• Accept an assurance that a solution exists
• Acknowledge production of solutions
• Some of the systems

Problems

• Use the TPTP
• Use non-biased TPTP problems
• Problem difficulty 0.21 to 0.99
• Preprocess to remove dependency on TPTP presentation
• Use unseen problems to negate tuning

Ranking

• Number of problems solved
• Number of problems solved with a solution proof output
• Break ties by average runtimes over solutions found.
• Measure SOTA contribution