CD Tools main page

Experiments with Combinatory Compression of Proof Structures (04-2022, 07-2022)

Experiments 1-3 are described in

Generating Compressed Combinatory Proof Structures - An Approach to Automated First-Order Theorem Proving
Christoph Wernhard
In Boris Konev, Claudia Schon, and Alexander Steen, editors, 8th Workshop on Practical Aspects of Automated Reasoning, PAAR 2022, CEUR Workshop Proceedings., 2022.

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

Result Tables

  1. Pure D-Term Proofs with Minimal Compacted Size
  2. Combinatory Compression of Given Proofs
  3. Proof Search with Combinatory Compression
  4. Exhaustive Search with CCS on the Real-First-Order Horn Problems in the TPTP


CD Tools main page