Proof Search with Combinatory Compression via Proof Schemas

This experiment shows results on proof search with combinatory compression via proof schemas on the TPTCD2 corpus. The prover configurations considered in this experiment explore the search space in full, that is, they do not apply any heuristic truncation of the search space such as, for example, by limiting the formula size of lemmas or by excluding different proofs of the same lemma.

Explanation of the Table Columns

All reported results were obtained on a HPC system with Intel(R) Xeon(R) Platinum 9242 CPU @ 2.30GHz CPUs and 3.7 GB of memory per CPU, and time limit per proving problem set to 2400s. Shown times are wall clock times in seconds.

Problem

The 196 problems of the TPTPCD2 corpus.

Rating

Problem rating according to latest value of the Rating field in TPTP 7.5.0.

#Ax

Number of axioms of the problem, not counting the condensed detachment meta-level axiom and the goal.

MC

Minimal compacted size of a proof of the problem if detected by exhaustive search with CCS in configuration M1 and configuration M2 (see also Experiment: Proofs with Minimal Compacted Size).

Columns shown for each considered configuration of CCS

SC

Compacted size of the returned proof schema term. Highlighting indicates that this value is less than the minimal compacted size for the problem according to column MC, or that that column is empty. The hyperlink leads to a graph representation of the proof.

Schemas

Proof schemas involving combinators that occur in the proof. The schemas basically considered are (in Prolog notation):

      (r0(P:1,Q:0):0)-[P,Q]
      (r1(P:2,Q:0,R:0):0)-[[P,Q],R]
      (r2(P:2,Q:0):1)-[P,Q]
      (r3(P:2,Q:0):1)-[[c,P],Q]
      (r4(P:1,Q:1):1)-[[b,P],Q]
      (r5(P:2,Q:1):2)-[[b,P],Q]
      (r6(P:2,Q:1):2)-[[b,[c,P]],Q]

For each proof, only schemas whose expansion involves a combinator are listed. Specifically, the obtained proof is rewritten with the following rules before the shown set of schemas occurring in it is determined:

    r0(X,Y)->[X,Y], r2(X,Y)->[X,Y], r1(i,X,Y)->[X,Y], [i,X]->X

Time

Time to find the proof.

XC

Compacted size of the proof after expanding the proof schemas and rewriting combinators to plain D-terms.

Considered configurations of CCS

S1+S2+S3

Best value from CCS in configurations S1–S3, according to values for columns C and, if these are equal, Time.

S1

CCS in configuration S1, with schemas r1,r2,r4,r5,r6.

S2

CCS in configuration S2, with schemas r1,r2,r3,r4,r5,r6.

S3

CCS in configuration S3, with schemas r0,r2,r4,r6.