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

Experiments and Studies

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

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

Experiments April 2022

These experiments are described in [W2022b].

Experiments January 2022

These experiments are described in [W2022a].

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

Publications

[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.
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 ]
[WB2023]
Investigations into Proof Structures
Christoph Wernhard and Wolfgang Bibel
2023
[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.
bib | Abstract ]
[W2022a]
CD Tools – Condensed Detachment and Structure Generating Theorem Proving (System Description)
Christoph Wernhard
Technical report, 2022.
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.
[ Preprint (extended version): https://arxiv.org/abs/2104.13645 | Presentation slides ]
bib | DOI | Abstract ]

Availability Experiments and Studies Publications

Contact: info@christophwernhard.com