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 [WB2024]
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
- horn_axioms_cd
- Axiom assignment: version for Horn clauses as axioms
- tabx_cd
- Conversion of D-terms to Tabx representation for interpolation
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
Metamath Interface
- mm_read
- Metamath: reading database file, database access predicates
- mm_form
- Metamath: formula parsing from sequence to term form
- mm_form_conversions
- Metamath: conversions of formulas between different formats
- mm_mmhammer_conversions
- Metamath: some conversions from/to MM-Hammer's format
- mm_access
- Metamath: interface to axioms, theorems and proofs
- mm_proof_conversions
- Metamath: proof conversions
- mm_proof_macros
- Metamath: proof macros
- mm_theorem_utils
- Metamath: various utilities to access theorems and axioms
- mm_addsyntax
- Metamath: completing proofs with parts for the syntax
- mm_proof_output
- Metamath: converting Metamath proof terms to Metamath syntax
- mm_tgr
- Metamath: proofs from the Metamath database as tree
grammars
Support for Tree Grammars
- tgr_utils
- Tree grammars: utility predicates
- tgr_treerepair
- Tree grammars: implementation of TreeRePair
- tgr_treerepair_replace
- Tree grammars: replacement phase of TreeRePair
- tgr_treerepair_prune
- Tree grammars: pruning phase of TreeRePair
- tgr_nonlin
- Tree grammars: compression by introducing non-linear rules
- tgr_sorting
- Tree grammars: ordering grammar rules
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
- fed_cd
- Utilities for factor compressed term
representations
Related Publications
[WB2024]
Investigations
into Proof Structures
Christoph
Wernhard and Wolfgang Bibel
Journal of
Automated Reasoning, 68(24), 2024.
[W2023]
Structure-Generating
First-Order Theorem Proving
Christoph
Wernhard
In Jens Otten and Wolfgang Bibel,
editors, AReCCa 2023 - Automated Reasoning with Connection Calculi,
International Workshop, volume 3613 of CEUR Workshop
Proceedings, pages 64-83. CEUR-WS.org, 2024.
[RWZB2023]
Lemmas:
Generation, Selection, Application
Michael
Rawson, Christoph Wernhard, Zsolt Zombori, and Wolfgang
Bibel
In Revantha Ramanayake and Josef Urban,
editors, Automated Reasoning with Analytic Tableaux and Related Methods:
32nd International Conference, TABLEAUX 2023, LNCS (LNAI). Springer,
2023.
[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.
[W2022a]
CD Tools – Condensed Detachment and
Structure Generating Theorem Proving (System
Description)
Christoph
Wernhard
Technical report,
2022.
[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.
CD Tools main page