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

arXiv: https://arxiv.org/abs/2207.08453 · HTML: https://mlsanity.com/paper/2207.08453/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 47 references that are in the map.
- First posted on arXiv 18 Jul 2022.

## Builds on (most cited first, 4 of 4)

- [Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report)](https://mlsanity.com/paper/2104.13138/) (2021)
- [Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic](https://mlsanity.com/paper/2002.10892/) (2020)
- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)
- [Craig Interpolation with Clausal First-Order Tableaux](https://mlsanity.com/paper/2008.03489/) (2020)

## Built on by (most cited first, 3 of 3)

- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)
- [Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving](https://mlsanity.com/paper/2209.12592/) (2022)
- [Investigations into Proof Structures](https://mlsanity.com/paper/2304.12827/) (2023)

## Abstract (arXiv)

CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP, which puts a recent formal view centered around proof structures into practice. From the viewpoint of first-order ATP, condensed detachment offers a setting that is relatively simple but with essential features and serious applications, making it attractive as a basis for developing and evaluating novel techniques. CD Tools includes specialized provers based on the enumeration of proof structures. We focus here on one of these, SGCD, which permits to blend goal- and axiom-driven proof search in particularly flexible ways. In purely goal-driven configurations it acts similarly to a prover of the clausal tableaux or connection method family. In blended configurations its performance is much stronger, close to state-of-the-art provers, while emitting relatively short proofs. Experiments show characteristics and application possibilities of the structure generating approach realized by that prover. For a historic problem often studied in ATP it produced a new proof that is much shorter than any known one.