SSCPA
Smart Selective Competition Parallelism ATP
ATP system performance data, e.g., the results of the
CADE ATP system competitions,
shows that no single sequential ATP system performs well on all problems.
There is convincing evidence that the specialisation of ATP systems is due
to the deduction techniques used in relation to the syntactic characteristics
of the problems.
This is well demonstrated with respect to the variety of deduction techniques
used by, e.g., Gandalf and Otter.
This observation provides the motivation for SSCPA's design.
SSCPA uses the syntactic characteristics of the given problem to classify
it into one of 18 predefined problem classes.
SSCPA then uses performance data from the available sequential ATP systems
to determine which of the systems perform well for that problem class.
The recommended systems are then run in parallel, in one of several user
selectable modes.
A WWW interface to SSCPA is available as part of
SystemOnTPTP.