Availability Experiments 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 a specialized prover called SGCD that is based on the enumeration of proof structures and combines goal- with axiom-driven search and another prover called CCS to experiment with the approach of compressed combinatory proof structures and DAG enumeration.

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

Experiments April 2022

Experiments January 2022

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

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

Contact: info@christophwernhard.com