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. CEUR-WS.org, 2022.
[ Preprint: http://cs.christophwernhard.com/papers/css.pdf ].

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

Archives

CD Tools main page