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 [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
dv_cd
Combinator-oriented operations on D-terms with variables
sk_cd
Support for combinator terms, also called SK-terms here

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

[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