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.

• 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

Experiments April 2022

• 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

Experiments January 2022

• The Condensed Detachment Problems in the TPTP
• 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

---

Availability Experiments Publications

Contact: info@christophwernhard.com