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].

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 Interface, August 2024

Modules of the Metamath interface
Short tests and examples
Draft of a system description: The Metamath Interface of CD Tools
An application:
Exploring Metamath Proof Structures
Christoph Wernhard and Zsolt Zombori
Presentation at AITP 2024
Abstract | Slides

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

[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 ]

[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.