CD Tools main page

CD Tools – Module Overview

This document lists the modules of CD Tools in groups with related or similar functionality. Module names link to the generated PlDoc documentation.

For background and explanation of terminology, e.g., D-term, compacted size (c-size), tree size (t-size), most general theorem (MGT) [aka principal type scheme], in-place theorem (IPT), n-simplification, ≥_c (c-comparison), prime D-term, see [WB2023] or [WB2021].

User Interface

working_cd: Re-exports various modules of CD Tools for a convenient working environment

D-terms (Proof Structures)

dterm_cd: Basic D-term operations
dterm_measures_cd: Various measures of D-terms
dc_representation_cd: Compressed printable representation of D-terms
gen_dterm_cd: Basic generator predicates for D-terms
c_comparison_cd: C-comparison of D-terms
random_cd: Construction of random D-terms
prime_cd: Support for prime D-terms
dy_cd: DY, a representation of a D-term that includes the IPTs at all positions
inspect_ipts_cd: Auxiliary predicates to inspect the IPTs of a D-term

F-terms (Formulas)

fterm_measures_cd: Various measures of F-terms
fterm_conversions_cd: Convert terms of formulas (F-terms) between different formats

Axioms

axioms_cd: Representation of the current axiom assignment (this module maintains a state)
named_axioms_cd: A compilation of named axioms

Regularities

regularity_cd: Various notions of regularity for D-terms
replace_cd: Replacing subterms of D-terms
organic_cd: The organic property for classical propositional logic

SGCD – A Structure Generating Prover for Condensed Detachment

sgcd_core_cd: SGCD prover core loop
sgcd_state_cd: Representation of the state maintained by SGCD prover (this module maintains a state)
sgcd_generators_cd: Generators for the SGCD prover
sgcd_initproofs_cd: Supplying initial lemmas to SGCD prover
sgcd_levelstest_cd: Tests to decide in the SGCD prover whether to keep generated proofs
sgcd_aux_cd: Auxiliary predicates for the SGCD prover
sgcd_newsprocessor_cd: Processing a newly generated level in the SGCD prover
sgcd_params_cd: Determine problem parameters for use by the SGCD prover

CCS – A Prover that Generates Compressed Combinatory Structures

ccs_main_cd: CCS prover: invocation
ccs_problem_cd: CCS prover: problem retrieval and preparation
ccs_setup_cd: CCS prover: argument setup from user specifications
ccs_compiler_cd: CCS prover: problem compilation
ccs_schema_support_cd: CCS prover: support to prepare proof schemas

Combinator-Oriented Representations and Techniques

combred_cd: Combinator reductions of D-terms
dv_cd: Combinator-oriented operations on D-terms with variables
sk_cd: Support for combinator terms, also called SK-terms here

Special Representations and Techniques

compress_cd: Grammar compression of D-terms with the TreeRePair tool

Conversions from other Systems

import_cd: Conversions from Prover9, KRHyper and CMProver proofs to D-terms
tptp_cd: Accessing condensed detachment problems in the TPTP

Pretty Printing and Visualization of Proofs

pp_cd: Printing D-terms in various ways
visualize_cd: Graph visualizations of D-terms
attributes_cd: Attributes of D-terms, mainly used for pretty printing proofs
dterm_conversions_cd: Format conversions for D-terms

Modules used for Experiments in 2020/21

luk_cd: Classic proofs for axiom Łukasiewicz
primecore_struct_lemmas_cd: PrimeCore structural lemmas
psp_struct_lemmas_cd: ProofSubproof structural lemmas
struct_lemmas_cd: General support for structural lemmas
luk_proofrepos_cd: Tables of stored proofs derived from Lukasiewicz's axiom
shorten_cd: Shortening of D-terms with a pool of precomputed small proofs
ds_remove_cd: Removing redundant D-terms from a list of D-terms

Building the Distribution and Documentation Pages

build_cd: Support for building a distribution or installation of cdtools

General Utilities

callutils_cd: Utilities to call a goal in special ways
compile_clauses_cd: Utilities to make code given as term effective
grounding_cd: Various ways to ground a given term and undo the grounding
infoutils_cd: Utilities to print information in human readable form
listutils_cd: Utility functions for lists
miscutils_cd: Miscellaneous utility functions
numutils_cd: Numeric utilities
trmutils_cd: General term utilities

Related Publications

[RWZB2023]

Lemmas: Generation, Selection, Application

Michael Rawson, Christoph Wernhard, Zsolt Zombori, and Wolfgang Bibel

TABLEAUX 2023

[ Preprint: https://arxiv.org/abs/2303.05854 ]

[WB2023]

Investigations into Proof Structures

Christoph Wernhard and Wolfgang Bibel

2023

[ Preprint: http://cs.christophwernhard.com/papers/investigations/ ]

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

[ Preprint: https://arxiv.org/abs/2209.12592 ].

[ bib | Abstract ]

[W2022a]

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

Christoph Wernhard

Technical report, 2022.

https://arxiv.org/abs/2207.08453.

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

CD Tools main page