Availability Experiments and Studies Publications

CD Tools

CD Tools is a Prolog library for experimenting with condensed detachment in automated first-order theorem proving, based on a recent formal view centered around proof structures [WB2021]. It includes two specialized provers: SGCD, based on the enumeration of proof structures and combining goal- with axiom-driven search [W2024]; CCS to experiment with the approach of compressed combinatory proof structures and DAG enumeration [W2022b]. It now also includes an interface to Metamath for experimenting with mathematical knowledge representation.

Particularly remarkable proofs obtained with the SGCD prover are a proof of LCL038-1 with compacted size 22 [W2022a,WB2024] and a proof of LCL073-1 [RWZB2023], a very hard problem for ATP that was by machine proven before only in 2000 by Wos in a specific workflow with OTTER. As D-term in DC representation, the proof of LCL038-1 is d(d(d(d(1,d(d(A,A),1)),1),1),1)-[A=d(1,d(d(B,1),B)),B=d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1)] and the proof of LCL073-1 is d(d(1,d(A,d(d(d(d(A,B),C),D),E))),d(F,d(F,1)))-[G=d(1,d(1,d(1,1))),H=d(1,I),I=d(1,J),K=d(1,d(B,d(1,d(d(1,d(C,d(C,d(d(D,J),I)))),1)))),F=d(1,d(A,d(1,d(A,H)))),J=d(G,G),B=d(H,1),L=d(H,B),D=d(d(1,d(1,d(I,E))),1),M=d(d(d(1,d(1,L)),B),1),E=d(M,d(1,C)),C=d(M,B),A=d(d(d(K,d(H,d(M,K))),1),L)].

Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – Project-ID 457292495. The work was supported by the North-German Supercomputing Alliance (HLRN).

Availability

CD Tools is published as free software under GNU General Public License. It runs with SWI-Prolog in the PIE environment, which provides basic support for first-order proving.

Obtaining the system
- By cloning its repository:
  $ git clone http://cs.christophwernhard.com/git/cdtools.git
- Or downloading an archive of the latest version in the repository
Module Overview (entry point to the system documentation)
Direct links to documents included in the distribution
- System Version | Changelog | ReadMe | License (GNU GPL)

Experiments and Studies

Metamath and Grammar-Compressed Proof Trees, May 2025

[WZ2025]: New comprehensive presentation, formal framework, experiments
Modules of the Metamath interface
- Short tests and examples
Modules for grammar-based tree compression

Metamath Interface, August 2024

[WZ2024]: An application
Modules of the Metamath interface

Short tests and examples
Draft of a system description: The Metamath Interface of CD Tools

Supplementary Material for Lemmas: Generation, Selection, Application [RWZB2023], March 2023

Sources: https://github.com/zsoltzombori/lemma
Result table

Supplementary Material for Investigations into Proof Structures, February 2023 [WB2024]

Supplementary material for the paper Investigations into Proof Structures [WB2024]

Experiments April 2022

These experiments are described in [W2022b].

Combinatory Compression of Proof Structures
- Pure D-term proofs with minimal compacted size
- Combinatory compression of given proofs
- Proof search with combinatory compression via proof schemas
- Exhaustive search with CCS on the real-first-order Horn problems in the TPTP (added July 2022)

Experiments January 2022

These experiments are described in [W2022a].

The Condensed Detachment Problems in the TPTP (Revised July 2022)
- Overview and times
- Proof dimensions
- Purely goal-driven proving
- Proofs with small compacted size (added July 2022)
68 Theses by Łukasiewicz in a Single Axiom-Driven Run
- Source
- Session transcript
A Short Proof for Łukasiewicz's Shortest Axiom
- Source
- Session transcript

Early Experiments 2021

These experiments with the problem ŁDS (= LCL038-1 in the TPTP) were performed in 2021 with a preliminary version of CD Tools and are described in [WB2021].

Result tables, original material to reproduce the experiments
Updated versions of the source files are included in the exp directory of the distribution.

Publications

[WZ2025]

Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures

Christoph Wernhard and Zsolt Zombori

Technical report, 2025.

https://arxiv.org/abs/2505.12305.

[ bib | DOI | Abstract ]

[WB2024]

Investigations into Proof Structures

Christoph Wernhard and Wolfgang Bibel

Journal of Automated Reasoning, 68(24), 2024.

[ Preprint: https://arxiv.org/abs/2304.12827 ].

[ bib | DOI | Abstract ]

[WZ2024]

Exploring Metamath Proof Structures (Extended Abstract)

Christoph Wernhard and Zsolt Zombori

In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, and Josef Urban, editors, 9th Conference on Artificial Intelligence and Theorem Proving, AITP 2024 (Informal Book of Abstracts), 2024.

[ Extended abstract | Presentation slides | Further material ].

[ bib ]

[W2024]

Structure-Generating First-Order Theorem Proving

Christoph Wernhard

In Jens Otten and Wolfgang Bibel, editors, AReCCa 2023 - Automated Reasoning with Connection Calculi, International Workshop, volume 3613 of CEUR Workshop Proceedings, pages 64-83. CEUR-WS.org, 2024.

[ Presentation slides ].

[ bib | .pdf | Abstract ]

[RWZB2023]

Lemmas: Generation, Selection, Application

Michael Rawson, Christoph Wernhard, Zsolt Zombori, and Wolfgang Bibel

In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, volume 14278 of LNCS (LNAI), pages 153-174. Springer, 2023.

[ Preprint (extended version): https://arxiv.org/abs/2303.05854 | Presentation slides ].

[ bib | DOI | Abstract ]

[W2022b]

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: https://arxiv.org/abs/2209.12592 ].

[ bib | Abstract ]

[W2022a]

CD Tools – Condensed Detachment and Structure Generating Theorem Proving (System Description)

Christoph Wernhard

Technical report, 2022.

https://arxiv.org/abs/2207.08453.

[ bib | DOI | Abstract ]

[WB2021]

Learning from Łukasiewicz and Meredith: Investigations into Proof Structures

Christoph Wernhard and Wolfgang Bibel

In André Platzer and Geoff Sutcliffe, editors, Automated Deduction: CADE 2021, volume 12699 of LNCS (LNAI), pages 58-75. Springer, 2021.