============================================================================== THGEN: Scripts and Code for Generating Theorems by Generating Proof Structures README.TXT Christoph Wernhard, March 2026 ============================================================================== OVERVIEW ======== THGEN is a collection of Bash scripts and SWI-Prolog programs that supplements the report [Christoph Wernhard: "Generating Theorems by Generating Proof Structures", 2026, https://arxiv.org/abs/2602.15511]. It contains edited extracts from the original Prolog code used for the described experiments that can serve to reproduce the experiments and as starting point for developing related experiments and applications. The functionality is accessible from Bash scripts which load short SWI-Prolog files that operate in the CD Tools environment (http://cs.christophwernhard.com/cdtools/overview.html). One possible way to become familiar with the functionality of CD Tools for new experiments and applications is by starting with the scripts, moving on to the short Prolog files that they load, and from there to the loaded documented modules of CD Tools (http://cs.christophwernhard.com/cdtools/overview.html). GENERAL NOTES ON THE SCRIPTS ============================ Some of the scripts take a sequence of arguments in the form of a Prolog list, which is passed to a Prolog predicate. For scripts that are invoked in the described experiments with different argument sequences we provide the lists of these argument sequences, one per line, in files *.lists, which are in the lists/ directory. These can be used to iterate over the argument sequences with shell commands or to process them in parallel with GNU parallel. Examples of both are given below. Square brackets "[", "]" in argument specifications express Prolog list notation instead of indicating optional arguments. The scripts were tested on a Linux server with four Intel Xeon E5-4640 processors (manufactured 2012-2015) and 256 GB RAM. Unless indicated otherwise, information on running times refers to this setting. A modern notebook is roughly twice as fast, but typically equipped with less RAM, which becomes critical in particular if experiments are invoked in parallel. TESTED VERSIONS =============== SWI-Prolog 10.0.0 CD Tools and PIE: as of 3 March 2026 Metamath database set.mm: Version July 5, 2025 (commit 011fba3), can be downloaded with: $ wget https://raw.githubusercontent.com/metamath/set.mm/011fba3f0cc4e1d2f7cfa62a6fd0694e07da10fc/set.mm LIST OF SCRIPTS =============== mk_poi_thm.sh - Generate POI theorems from set.mm mk_poi_tptp_problems.sh - Create TPTP problems for the POI theorems thgen_baserun.sh - Invoke SGCD bottom-up for the POI theorems thgen_prepare_dagsav.sh - Prepare lemma sequences thgen_addaxioms.sh - Invoke SGCD bottom-up with lemmas mk_addaxioms_lemma_file.sh - Create lemmas for further processing mk_addaxioms_tptp_problems.sh - Create lemma-enhanced TPTP problems thgen_comgen.sh - Run SGCD bottom-up with combinatory proof schemas mk_poi_thm_mmproof.sh - Convert Metamath proofs for implication form ============================================================================== SETUP ============================================================================== It is assumed that SWI-Prolog, PIE, CD Tools, and the TPTP are installed as described in README_METAMATH.TXT (http://cs.christophwernhard.com/cdtools/downloads/cdtools/README_METAMATH.TXT) In addition, the following environment variables are used by the scripts and should be set to installation-specific values. THGEN The thgen directory THGEN_OUT_DIR Directory for generated log and proof files THGEN_PLDATA_DIR Directory for large solution set files in gzipped SWi-Prolog's Fast Binary Term I/O format THGEN_DAGSAV_DIR Directory for generated Prolog files with lemmas In some example calls below, we also use ${LISTS} as shorthand for ${THGEN}/lists. However, the environment variable LISTS is not used by the scripts. ============================================================================== OUTPUT FILES OF SGCD RUNS ============================================================================== Invocations of SGCD with the scripts write, for each invocation of SGCD, various outputs to the directory THGEN_OUT_DIR. Proofs are there represented as DC-terms (dc_representation.pl), a special case of FSK-terms (sk_cd.pl, sk_mgt_cd.pl). For combinatory proof schemas, proofs are represented analogously but formed with pattern function symbols. The base names of these output files identify the run. The suffixes stand for the following kinds of files: .plcall: The top-level call. .benchlog (Prolog-readable): Facts benchlog(RunId, Property, KeyValList) with various information about the run, represented in KeyValList by Key=Value pairs. Information for a run is split into several facts with Property values: 'result_1', 'result_2' as well as 'done' or, for information about aborted runs, 'aborted'. .out: stdout and stderr .proofs (Prolog-readable): Representation of encountered proofs of POI theorems by facts found_proof(TheoremId, Proof). .lemmas (Prolog-readable): Representation of the proofs of supplied lemmas. Represented by facts lemma_proof(LemmaId, Proof). .pattinfo (Prolog-readable): Listing of patt_info/3 (see sgcd_patts_cd.pl). .patts_setting (Prolog-readable): Listing of patts_setting/1 (see sgcd_patts_cd.pl). ============================================================================== SCRIPTS ============================================================================== ------------------------------------------------------------------------------ NAME mk_poi_thm.sh - Generate POI theorems from set.mm SYNOPSIS $ mk_poi_thm.sh DESCRIPTION Write files /tmp/poi_thm.pl and /tmp/poi_thm_equiv.pl with predicate listings poi_thm/2 and poi_thm_equiv/2 for all POI theorems. These predicates are specified as follows. poi_thm(ThmId, Formula) ThmId is an atom, the theorem name (see mm_theorem/1) of a POI theorem. Formula is the theorem formula, canonicalized to implication form and grounded by grd_x/1. poi_thm_equiv(ThmId, ThmIds) ThmId is the theorem name of a POI theorem. ThmIds is the list of theorem names from set.mm whose canonicalized formula is identical to that of ThmId. NOTES Takes about 90 s (notebook). Outputs are also provided in ${THGEN}/prolog/generated/. ------------------------------------------------------------------------------ NAME mk_poi_tptp_problems.sh - Create TPTP problems for the POI theorems SYNOPSIS $ mk_poi_tptp_problems.sh DESCRIPTION Create a TPTP problem file in for each POI theorem. Determines the POI theorems in the same way as mk_poi_thm.sh. As side effect writes the predicate poi_thm_problem/2, which maps between theorem IDs and problem IDs to /tmp/poi_thm_problem.pl. NOTES The output for /tmp/poi_thm_problem.pl is also provided in ${THGEN}/prolog/generated/. The TPTP problems are also provided as http://cs.christophwernhard.com/cdtools/exp-thgen/downloads/poi_tptp.tgz ------------------------------------------------------------------------------ NAME thgen_baserun.sh - Invoke SGCD bottom-up for the POI theorems SYNOPSIS thgen_baserun.sh DESCRIPTION is a Prolog list of arguments. The first member is a symbolic (memnonic) identifier for the argument sequence, the second member is a predicate defined in thgen_baseruns.pl. The predicates called with the list where the second member is removed. The supported predicates are: - run_base_pldata: invokes SGCD bottom-up in a specific parameterization controlled by such that all generated solutions (i.e. level_solution/3 and abandoned_level_solution/4) are stored in gzipped Fast Binary Term I/O files. This allows (1) to generate runs with a large cardinality of abandoned_level_solution/4 that would exceed RAM, and (2) store generated solutions for re-use. - run_base: like run_base_pldata but keeping level_solution/3 and abandoned_level_solution/4 as predicates in main memory. - run_incbase: invokes SGCD bottom-up in a specific parameterization controlled by that essentially just restricts considered proof terms by the size of their MGT. EXAMPLE $ parallel -j 10 thgen_baserun.sh {1} :::: ${LISTS}/baserun_test.list Takes a few seconds. EXPERIMENT: Generating POI Base $ parallel -j 2 thgen_baserun.sh {1} :::: ${LISTS}/baserun_large.list Takes about 6:45 hours. $ parallel -j 10 thgen_baserun.sh {1} :::: ${LISTS}/baserun_inc.list Takes about 1:20 hours. EXPERIMENT: Generating Base Sets for Lemma Synthesis $ parallel -j 10 thgen_baserun.sh {1} :::: ${LISTS}/baserun_lemmas.list Takes about 2:00 hours. The outputs are also provided as http://cs.christophwernhard.com/cdtools/exp-thgen/downloads/thgen_pldata.tar ------------------------------------------------------------------------------ NAME thgen_prepare_dagsav.sh - Prepare lemma sequences SYNOPSIS thgen_prepare_dagsav.sh [,] DESCRIPTION Calls the predicate prepare_dagsav_file/1 in thgen_dagsav.pl, which performs DAG compression for a set of proof terms and writes the resulting sequence of lemmas to a file. NOTES and must be defined in thgen_dagsav.pl with define_dagsav_ax_src/2 and define_dagsav_ax_key/2, respectively. For the sources configured for , pldata files must be present in THGEN_PLDATA_DIR, e.g., ls_small_tsize.pldata.gz, as_small_tsize.pldata.gz. These can be generated with thgen_baserun.sh for the entries in baserun_lemmas.list, or, alternatively, downloaded from http://cs.christophwernhard.com/cdtools/exp-thgen/downloads/thgen_pldata.tar EXAMPLE Successive invocation for all lemma sequences used in runs S1-S13: $ for a in `cat ${LISTS}/dagsav.list`; do thgen_prepare_dagsav.sh $a; done Takes 13 minutes (notebook), or 32 minutes (server). ------------------------------------------------------------------------------ NAME thgen_addaxioms.sh - Invoke SGCD bottom-up with lemmas SYNOPSIS thgen_addaxioms.sh DESCRIPTION is a Prolog list with parameters of the SGCD run. The first member is an symbolic (memnonic) identifier of the run. For the used lemma sequences, dagsav files prepared by thgen_prepare_dagsav.sh must be present in THGEN_DAGSAV_DIR, e.g., dagsav_lms_k_sav.pl. EXAMPLE $ parallel -j 10 thgen_addaxioms.sh {1} :::: ${LISTS}/addaxioms_test.list Takes a few seconds. EXPERIMENT: Runs S1-S13 $ parallel -j2 thgen_addaxioms.sh {1} :::: ${LISTS}/addaxioms.list Takes 6:40 hours ------------------------------------------------------------------------------ NAME mk_addaxioms_lemma_file.sh - Create lemmas for further processing SYNOPSIS mk_addaxioms_lemma_file.sh [,,,] Compute a sequence of lemmas as with thgen_addaxioms.sh and extract their formulas into a predicate for further processing, e.g., to generate inputs for first-order provers with mk_addaxioms_tptp_problems.sh. The arguments can be a longer list, e.g., a list used for thgen_addaxioms.sh, in which case only the first four list members are considered. The output has a single fact with meta information, e.g.: lemma_info([pretty_id=test, card=10, src_id=lms, key_id=k_sav]). And for each lemma a fact with the formula, e.g.: lemma(((A=>B)=>((C=>A)=>(C=>B)))). lemma((((_=>A)=>B)=>(A=>B))). The listings of lemma_info/1 and lemma/1 are written to stdout. EXAMPLE $ mk_addaxioms_lemma_file.sh [lemtest,50,lms,k_sav] >/tmp/lemmas1.pl ------------------------------------------------------------------------------ NAME mk_addaxioms_tptp_problems.sh - Create lemma-enhanced TPTP problems SYNOPSIS $ mk_addaxioms_tptp_problems.sh DESCRIPTION is as obtained by mk_addaxioms_lemma_file.sh. Creates a directory with a lemma-enhanced TPTP problem for each POI theorem. The problem names are the same as those for mk_poi_tptp_problems.sh, but now placed in a subdirectory of whose name indicates the respective lemma settings: /poi_tptp____/ The respective information is taken from the lemma_info/1 fact in . NOTES Example outputs with the problems described in the report are provided as http://cs.christophwernhard.com/cdtools/exp-thgen/downloads/poi_tptp_lemmas.tgz (685 KB, expands into 6 MB). ------------------------------------------------------------------------------ NAME thgen_comgen.sh - Run SGCD bottom-up with combinatory proof schemas SYNOPSIS thgen_combgen.sh DESCRIPTION Calls the predicate patt_psp/2 defined in thgen_combgen.pl, which performs an SGCD bottom-up run with combinatory proof schemas. is a Prolog list of arguments, parameters of the SGCD run. The first member is an symbolic (memnonic) identifier of the run. EXAMPLE $ parallel -j 10 thgen_combgen.sh {1} :::: ${LISTS}/combgen_test.list Takes a few seconds. EXPERIMENT: Runs C1-C22. $ parallel -j4 thgen_combgen.sh {1} :::: ${LISTS}/combgen.list Takes about 1:45 hours. ------------------------------------------------------------------------------ NAME mk_poi_thm_mmproof.sh - Convert Metamath proofs for implication form SYNOPSIS $ mk_poi_thm_mmproof.sh DESCRIPTION Write facts poi_thm_mmproof(, ) with converted versions of the proofs from set.mm for all POI theorems to stdout. The proofs: - Prove the theorem statement in implication form. I.e. from the first-order point of view a unit clause with object-level implications. This involves lambda-to-SK translation. - Have only 1,2,3 (corresponding to ax-1, ax-2, ax3 in set.mm) as axioms. Any definitional axioms are translated to proofs of corresponding theorems as indicated in comments of set.mm. - Are represented as DC-terms (dc_representation.pl), a special case of FSK-terms (sk_cd.pl, sk_mgt_cd.pl). Skips theorems whose proofs have very large tree size (> 10^7), and thus gives proofs for only 1297 of the 1374 POI theorems. EXAMPLE $ mk_poi_thm_mmproof.sh >/tmp/poi_thm_mmproof.sh Takes about 2 min (notebook). The output is also provided as http://cs.christophwernhard.com/cdtools/exp-thgen/downloads/poi_proofs_setmm.pl