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.
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.
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].
Contact: info@christophwernhard.com