TPTP-CASC-SSCPA
Abstract
This seminar gives an overview of three interelated projects:
- TPTP
- The Thousands of Problems for Theorem Provers Problem
Library is a library of test problems for automated theorem
proving (ATP) systems.
The TPTP supplies the ATP community with a comprehensive library
of the ATP test problems that are available today.
The principal aim of this project is to move the evaluation
of ATP systems from the previously ad hoc situation onto a firm
footing.
This became necessary, as results being published do not always
accurately reflect the capabilities of the ATP system being
considered.
- CASC
- The CADE ATP System Competition is an annual event that
evaluates ATP systems in terms of their ability to solve problems
chosen from the TPTP.
Besides the obvious aim of evaluating ATP systems, CASC stimulates
ATP research and implementation of working autonomous ATP systems,
provides an inspiring environment for personal interaction between
ATP researchers, and exposes ATP systems to researchers both within
and outside the ATP community.
- SSCPA
- The Smart Selective Competition Parallelism ATP system is
an uncooperative multiple calculus competition parallelism ATP
system, that multitasks on a single CPU.
SSCPA runs multiple sequential ATP systems in parallel, using
performance data from the ATP systems to select those that are
best suited to the problem.
As a meta-system, SSCPA outperformed all other systems in the
MIX and SAT divisions of CASC-16.