Lemmas: Generation, Selection, Application – Results

This table shows individual results of the experiments described in Michael Rawson, Christoph Wernhard, Zsolt Zombori and Wolfgang Bibel: Lemmas: Generation, Selection, Application – Results, 2023 (Preprint).

• The -TC versions of TPTP problems are single-axiom versions obtained with Tarski's technique as described in Tarski's Claim thirty years later, 2010, in A. Rezus: Witness Theory – Notes on λ-calculus and Logic, 2020, pp. 217–225.
• For each proof, if it is a D-term (i.e. a condensed detachment proof), its dimensions are shown as
  Compacted Size / Tree Size / Height.
• Proof sizes are shown after n-simplification. The prefix n before the dimensions indicates that n-simplification had a size-reducing effect.
• Reported times refer for setups with lemma generation just to the last prover invocation, ignoring the time of lemma generation, learning and lemma selection.
• An empty cell indicates that the problem could not be solved by the respective prover or configuration.
• The problems are from TPTP 8.1.2. Ratings refer to the latest value of the problem's Rating field in TPTP 8.1.2.

Prover Setups

An asterisk (*) indicates that the setup involves lemma application. The suffix indicates the selection method for the lemmas: -LIN* learning with a linear model, -GNN* learning with a GNN model, -LIN-GNN* learning with a combined linear/GNN model, -HEU-X* lemma selection by sorting according to heuristic features.

Best Proof

The best proof according to the following ordering, applied lexically: prefer if it is a D-term (i.e. condensed detachment proof), compacted size, tree size, height, prefer if n-simplification did not effect a size reduction, prefer if without lemma application, reported time. Thus, proofs for which no D-term representation was available were here ranked worse and their size is not considered. The respective prover is also shown. The comparison for prefer if without lemma application immediately before reported time has the purpose of taking into account that in reported time the time for lemma generation, learning and lemma selection is ignored. Also some results for special configurations with heuristic lemma selection are included, indicated by the following prover names: Prover9-HEU-1* is Prover9 with 1,000 PSP optim input lemmas, Vampire-HEU-2* is Vampire with 1,000 PSP plain input lemmas and SGCD-HEU-3* is a special setup described in our paper.

SGCD-1

SGCD in a portfolio configuration without lemmas. Used as basis for SGCD-LIN*.

SGCD-LIN*

SGCD in a portfolio configuration with iterative improvement through learned lemmas.

Prover9

Prover9 without lemmas.

Prover9-LIN*

Prover9 with iterative improvement through learned lemmas.

Vampire

Vampire in casc portfolio mode without lemmas.

Vampire-LIN*

Vampire in casc portfolio mode enhanced with lemmas.

E

E in auto-schedule configuration without lemmas.

E-LIN*

E in auto-schedule configuration enhanced with lemmas.

leanCoP

leanCoP without lemmas.

leanCoP-LIN*

leanCoP enhanced with lemmas.

CMProver

CMProver in a portfolio configuration without lemmas.

CMProver-LIN*

CMProver in a portfolio configuration with iterative improvement through learned lemmas.

CCS-Vanilla

CCS-Vanilla without lemmas.

CCS-Vanilla-LIN*

CCS-Vanilla with iterative improvement through learned lemmas.

SGCD-2

SGCD without lemmas in a portfolio configurations. Used as basis for SGCD-GNN*. Same setup as SGCD-1 but slightly different results due to system fluctuations.

SGCD-GNN*

SGCD in a portfolio configuration with iterative improvement through learned lemmas.

SGCD-3

SGCD without lemmas in a portfolio configurations. Used as basis for SGCD-LIN-GNN*. Same setup as SGCD-1 and SGCD-2 but slightly different results due to system fluctuations.

SGCD-LIN-GNN*

SGCD in a portfolio configuration with iterative improvement through learned lemmas.