CD Tools main page

TPTPCD/SGCD Experiments: The Condensed Detachment Problems in the TPTP

TPTP 8.0.0 contains 206 condensed detachment problems, all in the LCL domain. Corpus TPTPCD2 is the subset of those 196 problems that remain after excluding problems of the following types: Problems with a form of detachment for disjunction and negation instead of implication, problems known as satisfiable, and problems with multiple goal theorems.

These experiments show the performance of the SGCD prover included in CD Tools on the TPTPCD2 corpus, in various configurations, and in comparison to selected other provers.

The experiments are described in

CD Tools – Condensed Detachment and Structure Generating Theorem Proving (System Description)
Christoph Wernhard
Technical report, 2022.
bib | DOI | Abstract ]

The work was supported by the North-German Supercomputing Alliance (HLRN).

Result Tables


Earlier Version of the Experiments

CD Tools main page