%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Copyright (C) 2023 Christoph Wernhard %%%% %%%% This program is free software: you can redistribute it and/or modify it %%%% under the terms of the GNU General Public License as published by the %%%% Free Software Foundation, either version 3 of the License, or (at your %%%% option) any later version. %%%% %%%% This program is distributed in the hope that it will be useful, but %%%% WITHOUT ANY WARRANTY; without even the implied warranty of %%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General %%%% Public License for more details. %%%% %%%% You should have received a copy of the GNU General Public License along %%%% with this program. If not, see . %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Overview %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% This code accompanies the paper "Investigations into Proof Structures" by %%%% Christoph Wernhard and Wolfgang Bibel, 2023. %%%% Preprint: https://arxiv.org/abs/XXX %%%% %%%% The code uses the CD Tools environment, which realizes concepts and %%%% techniques discussed in the paper. It is available from %%%% %%%% http://cs.christophwernhard.com/cdtools/ %%%% %%%% Its main purposes are: %%%% %%%% - Making the experimental results in the paper reproducible. %%%% %%%% - Illustrating how concepts and results of the paper can be transferred %%%% into a practical system. %%%% %%%% - Providing examples and starting points for using various components of %%%% CD Tools in further research. %%%% %%%% The code runs in SWI-Prolog with CD Tools, which in turn is based on PIE %%%% http://cs.christophwernhard.com/pie/. All requirements are free software. %%%% %%%% The following additional software is recommended: An installation of the %%%% TPTP (https://www.tptp.org/) with the environment variable %%%% "TPTPDirectory" proprly set, Prover9 including ProofTrans, and %%%% TreeRePair. See the installation notes on CD Tools for further %%%% information: %%%% http://cs.christophwernhard.com/cdtools/downloads/cdtools/README.TXT %%%% %%%% The code has been tested with SWI-Prolog 9.0.3 and versions of CD Tools %%%% and PIE from February 2023. %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Quickstart %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Load this file into CD tools. Run all experiments that do not require %%%% more than 10 seconds each (expected time) with %%%% %%%% ?- run_all(10). %%%% %%%% Run a particular experiment, without time restriction, for example: %%%% %%%% ?- set_maxtime(-1). %%%% ?- exp(sect(3)-1). %%%% %%%% Run all experiments, including those that take a longer time (needs about %%%% 15-30 min) with: %%%% %%%% ?- run_all(-1). %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- use_module(cdtools(axioms_cd)). :- use_module(cdtools(c_comparison_cd)). :- use_module(cdtools(callutils_cd)). :- use_module(cdtools(ccs_main_cd)). :- use_module(cdtools(compress_cd)). :- use_module(cdtools(dterm_cd)). :- use_module(cdtools(dy_cd)). :- use_module(cdtools(fterm_conversions_cd)). :- use_module(cdtools(fterm_measures_cd)). :- use_module(cdtools(gen_dterm_cd)). :- use_module(cdtools(grounding_cd)). :- use_module(cdtools(import_cd)). :- use_module(cdtools(luk_cd)). :- use_module(cdtools(miscutils_cd), [sub_term_u/2]). :- use_module(cdtools(named_axioms_cd)). :- use_module(cdtools(numutils_cd)). :- use_module(cdtools(prime_cd)). :- use_module(cdtools(regularity_cd)). :- use_module(cdtools(replace_cd)). :- use_module(cdtools(sgcd_core_cd)). :- use_module(cdtools(sk_cd)). :- use_module(cdtools(tptp_cd)). :- use_module(swilib(err)). :- use_module(swilib(info)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- discontiguous exp/1. :- dynamic exp_maxtime/1. :- initialization(set_maxtime(10)). %%%% %%%% Run all experiments that are expected to finish in ExpMaxtime seconds %%%% (per experiment). Run them without this restriction if ExpMaxtime is -1. %%%% run_all(ExpMaxtime) :- set_maxtime(ExpMaxtime), ( clause( exp(E), _ ), format('========================================'), format('======================================~n'), format('Experiment ~w~n', [E]), format('========================================'), format('======================================~n'), exp(E), fail ; true ). %%%% %%%% Set to -1 to let all individual experiments run without checking the %%%% estimated time requirement. %%%% set_maxtime(T) :- retractall( exp_maxtime(_) ), asserta( exp_maxtime(T) ). requirements(R) :- ( member(R1, R), \+ holds_requirement(R1) -> format('Skipping experiment due to failed requirement: ~q~n', [R1]), fail ; true ). holds_requirement(tptp) :- !, getenv('TPTPDirectory', _), !. holds_requirement(prover9) :- !, shell('which prover9 >/dev/null', 0), shell('which prooftrans >/dev/null', 0). holds_requirement(treerepair) :- !, shell('which TreeRePair >/dev/null', 0). holds_requirement(time(T)) :- !, exp_maxtime(TM), ( TM =< 0 -> true ; T =< TM ). expinfo(X) :- format('Relates to ~w~n', [X]), format('----------------------------------------'), format('--------------------------------------~n'). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Section 3: Basic examples of CD proofs %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% The proof of Figure 2 and Examples 2,3,6,8 for axiom syll_simp %%%% examp_d(D) :- D = d(d(1,1),d(d(1,d(1,1)),d(1,d(1,1)))). exp(sect(3)-1) :- expinfo('proof in Fig. 2 and Examples 2,3,6,8 for axiom Syll-Simp'), install_named_axiom(syll_simp), examp_d(D), format('The D-term: ~q~n', [D]), d_tsize(D, TS), d_height(D, HS), d_csize(D, CS), format('Measures - tree size: ~d, height: ~d, compacted size: ~d~n', [TS, HS, CS]), setof(D1, (sub_term(D1, D), compound(D1)), SubDs), format('Compound Subterms:~n'), pp(SubDs), nl, format('The D-term in factor notation (as in Fig. 2c and Example 8):~n'), pp_sk(D, [fact=1,style=dterm,vstart=2,vhead='']), d_mgt(D, F), f_to_cf(F, CF), f_to_if(F, IF), char_code(p, KP), char_code(a, KA), KP1 is KP-KA, numbervars(F, KP1, _), format('The proven formula in different notations:~n'), format('Łukasiewicz\'s notation: ~w~n', [CF]), format('Term notation with i/2: ~q~n', [IF]), format('CDTools notation: ~q~n', [F]). exp(sect(3)-2) :- expinfo('Table 1'), install_named_axiom(true), F = '~|Number of D-terms of ~w~t ~D:~40+~|~t ~D~10+~n', ( between(0, 5, I), nsols(gen_d_of_tsize(I,_), N), format(F, ['tree size', I, N]), fail ; true ), ( between(0, 5, I), nsols(gen_d_of_height(I,_), N), format(F, [height, I, N]), fail ; true ), ( between(0, 5, I), nsols(gen_d_of_csize(I,_), N), format(F, ['compacted size', I, N]), fail ; true ). exp(sect(3)-3) :- expinfo('Example 25'), named_axiom(simp, A), install_axioms([1-A], []), D1 = d(1,1), d_mgt(D1, F1), char_code(p, KP), char_code(a, KA), KP1 is KP-KA, numbervars(F1, KP1, _), format('~|MGT of ~q:~t~48+~q~n', [D1, F1]), D2 = d(d(1,1),1), d_to_dy(D2, DY), once(dy_sub_term(DY, D1, F2)), numbervars(F2, KP1, _), format('~|IPT of the occurrence of ~q in ~q:~t~48+~q~n', [D1, D2, F2]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Section 4: Compaction orderings %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% c_compare(D1, D2, C) :- ( c_greater(D1, D2) -> C = '>_c' ; c_greater(D2, D1) -> C = '<_c' ; c_greaterq(D1, D2) -> C = '>=_c' ; c_greaterq(D2, D1) -> C = '<=_c' ; C = '--' ). exp(sect(4)-1) :- expinfo('text following Definition 30 and Examples 32, 34'), Pairs = [d(d(d(1,1),1),1)-d(1,d(1,1)), 1-d(1,1), d(1,d(1,d(1,1)))-d(d(1,d(1,1)),1), d(1,d(1,d(1,1)))-d(d(1,1),1), d(1,d(1,d(1,d(1,1))))-d(d(1,d(1,1)),d(1,d(1,1))), d(1,d(2,d(3,3)))-d(4,d(3,3)), d(1,d(1,d(1,d(1,1))))-d(1,d(d(1,1),1)), d(1,d(2,d(3,3)))-d(4,d(5,5)) ], ( member(D1-D2, Pairs), c_compare(D1, D2, C), format('~|~q~t~22+~|~w~4+ ~q~n', [D1, C, D2]), fail ; true ). d_scsize(D, N) :- setof(S, (sub_term(S,D)), Y), d_sfs(Y, 0, N1), N = N1. d_sfs([], N, N). d_sfs([D|Ds], N, N1) :- d_csize(D, N2), N3 is N+N2, d_sfs(Ds, N3, N1). exp(sect(4)-2) :- expinfo('Examples 36, 37'), D0 = d(d(d(1,1),d(1,1)),d(d(1,1),1)), d_scsize(D0, S), format('sc size of ~q: ~w~n', [D0, S]), D1 = d(d(d(d(d(1,1),1),1),1),d(1,d(1,d(1,d(1,1))))), E1 = d(d(d(d(d(d(d(1,1),1),1),1),1),1),1), d_csize(D1, CD1), d_csize(E1, CE1), d_scsize(D1, SD1), d_scsize(E1, SE1), format('c-sizes: ~w ~w, sc-sizes: ~w ~w~n', [CD1, CE1, SD1, SE1]). exp(sect(4)-3) :- expinfo('Example 39'), D = d(d(1,d(1,1)),d(1,d(1,d(1,1)))), D1 = d(d(1,d(1,1)),d(d(1,1),1)), E = d(1,d(1,d(1,1))), E1 = d(d(1,1),1), %% verify claimed properties d_replace_all(D, E, E1, D2), D1 == D2, c_greater(E, E1), %% d_csize(D, CD), d_csize(D1, CD1), format('Compacted sizes: ~d ~d~n', [CD, CD1]), d_scsize(D, SD), d_scsize(D1, SD1), format('SC sizes: ~d ~d~n', [SD, SD1]). exp(sect(4)-4) :- expinfo('Example 40'), D = d(d(d(1,d(1,d(1,1))),1),d(d(1,d(1,d(1,1))),1)), D1 = d(d(d(1,d(1,1)),1),d(d(1,d(1,1)),1)), D2 = d(d(d(1,d(1,1)),1),d(d(1,d(1,d(1,1))),1)), E = d(1,d(1,1)), E1 = d(1,1), %% verify claimed properties d_replace_all(D, E, E1, D3), D1 == D3, %% d_csize(D, CD), d_csize(D1, CD1), format('Compacted sizes: ~d ~d~n', [CD, CD1]), %% verify claimed properties once(d_replace_one(D, E, E1, D4)), D2 == D4, %% d_csize(D2, CD2), format('Compacted sizes: ~d ~d~n', [CD, CD2]). exp(sect(4)-5) :- expinfo('Proposition 41'), install_axioms([1-_,2-_,3-_], [quiet]), ( between(1, 5, I), format('Checking D-terms of tree size ~w~n', [I]), gen_d_of_tsize(I, D), prop_41_leftside(D, NL), prop_41_rightside(D, NR), NL \= NR -> format('Found counterexample for Prop. 41~n') ; format('Found no counterexample for Prop. 41~n') ). prop_41_leftside(D, N) :- setof(E, gen_c_smallerq(D, E), Es), length(Es, N). prop_41_rightside(D, N) :- setof(A, (sub_term(A, D), atomic(A)), As), length(As, NP), d_csize(D, CS), N is (CS - 1 + NP)^2 + NP. exp(sect(4)-6) :- expinfo('Examples 48, 49'), ( ( A = syll_simp, D = d(d(d(1,1),1),1) ; A = luk, D = d(d(d(d(1,d(1,1)),1),1),d(1,1)) ), install_named_axiom(A), format('Axiom: ~w D-term: ~w~n', [A, D]), show_regularity(D), fail ; true ). show_regularity(D) :- ( d_is_regular(ipt_ipt, D) -> IS = yes ; IS = no ), ( d_is_regular(mgt_mgt, D) -> MS = yes ; MS = no ), ( d_is_regular(ipt_mgt, D) -> S = yes ; S = no ), format('Regularity wrt. IS: ~w; MS: ~w; S: ~w~n', [IS, MS, S]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Section 5: The Proofs by Łukasiewicz and Meredith %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Transliterations of the proofs by Łukasiewicz and Meredith are provided %%%% in module luk_cd.pl, in particular with predicates luk_lemma/3 and %%%% mer_lemma/4. %%%% %%%% The proofs as a list of D-terms (proofs of syll, peirce and simp) are %%%% available as luk_ds/1 and mer_ds/1. After n-simplification as luk_ds_n/1 %%%% and mer_ds_n/1. %%%% %%%% The number labeling of subproofs is available as luk_d/2 and mer_d/2 (or %%%% mer_dx/2 with extra labels 10.5 and 16.5, the latter for MER16'). After %%%% n-simplification as luk_d_n/2 and mer_d_n/2. %%%% %%%% %%%% %%%% exp(sect(5)-1) :- expinfo('Section 5.4.1 DC, DT, DH: Comapcted Size, Tree Size and Height'), install_named_axiom(luk), luk_ds(DsLuk0), mer_ds(DsMer0), ds_simp_n(DsLuk0, DsLuk), ds_simp_n(DsMer0, DsMer), DsLuk = [DSyllLuk|_], DsMer = [DSyllMer|_], format('--------------------------------------------------------------------~n'), format('Dimensions of the subproof of Syll~n'), format('--------------------------------------------------------------------~n'), d_csize(DSyllLuk, DC_DSyllLuk), d_csize(DSyllMer, DC_DSyllMer), d_tsize(DSyllLuk, DT_DSyllLuk), d_tsize(DSyllMer, DT_DSyllMer), d_height(DSyllLuk, DH_DSyllLuk), d_height(DSyllMer, DH_DSyllMer), format('DC (compacted size) Mer: ~w Łuk: ~w~n', [DC_DSyllMer, DC_DSyllLuk]), format('DT (tree size) Mer: ~w Łuk: ~w~n', [DT_DSyllMer, DT_DSyllLuk]), format('DH (height) Mer: ~w Łuk: ~w~n', [DH_DSyllMer, DH_DSyllLuk]), DsLuk0 = [DSyllLuk0|_], DsMer0 = [DSyllMer0|_], format('--------------------------------------------------------------------~n'), format('Dimensions of the subproof of Syll - before n-simplification~n'), format('--------------------------------------------------------------------~n'), format('Before n-simplification~n'), d_csize(DSyllLuk0, DC_DSyllLuk0), d_csize(DSyllMer0, DC_DSyllMer0), d_tsize(DSyllLuk0, DT_DSyllLuk0), d_tsize(DSyllMer0, DT_DSyllMer0), d_height(DSyllLuk0, DH_DSyllLuk0), d_height(DSyllMer0, DH_DSyllMer0), format('DC (compacted size) Mer: ~w Łuk: ~w~n', [DC_DSyllMer0, DC_DSyllLuk0]), format('DT (tree size) Mer: ~w Łuk: ~w~n', [DT_DSyllMer0, DT_DSyllLuk0]), format('DH (height) Mer: ~w Łuk: ~w~n', [DH_DSyllMer0, DH_DSyllLuk0]), format('--------------------------------------------------------------------~n'), format('Dimensions of the overall proof~n'), format('--------------------------------------------------------------------~n'), ds_csize(DsMer, CSMer), ds_csize(DsLuk, CSLuk), ds_tsize(DsMer, TSMer), ds_tsize(DsLuk, TSLuk), ds_height(DsMer, HSMer), ds_height(DsLuk, HSLuk), format('Overall compacted size Mer: ~w Łuk: ~w~n', [CSMer, CSLuk]), format('Overall tree size Mer: ~w Łuk: ~w~n', [TSMer, TSLuk]), format('Overall height Mer: ~w Łuk: ~w~n', [HSMer, HSLuk]), format('--------------------------------------------------------------------~n'), format('Dimensions of the overall proof - before n-simplification~n'), format('--------------------------------------------------------------------~n'), ds_csize(DsMer0, CSMer0), ds_csize(DsLuk0, CSLuk0), ds_tsize(DsMer0, TSMer0), ds_tsize(DsLuk0, TSLuk0), ds_height(DsMer0, HSMer0), ds_height(DsLuk0, HSLuk0), format('Overall compacted size Mer: ~w Łuk: ~w~n', [CSMer0, CSLuk0]), format('Overall tree size Mer: ~w Łuk: ~w~n', [TSMer0, TSLuk0]), format('Overall height Mer: ~w Łuk: ~w~n', [HSMer0, HSLuk0]). exp(sect(5)-2) :- expinfo('Section 5.4.5 DP: Is Prime'), install_named_axiom(true), ( between(0, 7, I), nsols( gen_d_mgt_prime_of_size(I, _, _), N ), format('Number of prime dterms at level ~w: ~w~n', [I, N]), fail ; true ), install_named_axiom(luk), mer_d(6, D), d_mgt(D, F), grd_p(F), format('Trying to prove ~w from luk by prime level enumeration~n', [F]), ( between(0, 100, I), gen_d_mgt_prime_of_size(I, D1, F) -> format('Found prime proof at level ~w:~n ~w~n', [I, D1]) ; format('Found no prime proof~n') ). exp(sect(5)-3) :- expinfo('Section 5.6.1'), install_named_axiom(luk), mer_ds_n([_, DPeirceMer, DSimpMer]), luk_ds_n([_, DPeirceLuk, DSimpLuk]), d_tsize(DSimpMer, DTDSimpMer), d_tsize(DSimpLuk, DTDSimpLuk), d_csize(DSimpMer, DCDSimpMer), d_csize(DSimpLuk, DCDSimpLuk), format('Proof of simp in Mer - tree size: ~w compacted size: ~w~n', [DTDSimpMer, DCDSimpMer]), format('Proof of simp in Łuk: - tree size: ~w compacted size: ~w~n', [DTDSimpLuk, DCDSimpLuk]), named_axiom(simp, Simp), grd_p(Simp), ( between(0, 100, IT), gen_d_mgt_of_tsize(IT, DTSimp, Simp) -> format('Found proof of simp with min. tree size ~w:~n ~w~n', [IT, DTSimp]) ; format('Found no tree-size-based proof of simp') ), ( between(0, 100, IC), gen_d_mgt_of_csize(IC, DCSimp, Simp) -> format('Found proof of simp with min. compacted size ~w:~n ~w~n', [IC, DCSimp]) ; format('Found no compacted-size-based proof of simp') ), d_tsize(DPeirceMer, DTDPeirceMer), d_tsize(DPeirceLuk, DTDPeirceLuk), d_csize(DPeirceMer, DCDPeirceMer), d_csize(DPeirceLuk, DCDPeirceLuk), format('Proof of peirce in Mer - tree size: ~w compacted size: ~w~n', [DTDPeirceMer, DCDPeirceMer]), format('Proof of peirce in Łuk: - tree size: ~w compacted size: ~w~n', [DTDPeirceLuk, DCDPeirceLuk]), named_axiom(peirce, Peirce), grd_p(Peirce), ( between(0, 100, ITP), gen_d_mgt_of_tsize(ITP, DTPeirce, Peirce) -> format('Found proof of peirce with min. tree size ~w:~n ~w~n', [ITP, DTPeirce]) ; format('Found no tree-size-based proof of peirce') ). exp(sect(5)-4) :- %% Takes a few minutes. expinfo('Section 5.6.1'), requirements([time(300)]), requirements([longtime]), named_axiom(luk, Luk), named_axiom(peirce, Peirce), grd_p(Peirce), Problem = cd_problem(Peirce, [Luk]), format('Running the CCS prover in vanilla configuration to find~n'), format('a proof of peirce with min. compacted size.~n'), format('This takes about 180-400 s.~n'), get_time(T1), ccs(Problem, [format=cd, gen=[d(_,_)], once=once, proof=D]), get_time(T2), T is T2 - T1, format('Used time ~2fs~n', [T]), d_csize(D, SC), format('Found proof of peirce with min. compacted size ~w~n ~w~n', [SC, D]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Section 6.2: Prover9's proofs and reductions by replacing subproofs %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Calling Prover9 for CD problems via PIE. Requires prover9, including %%%% prooftrans to be installed. %%%% tptpcd_prover9_proof(P, Timeout, D, Options) :- tptpcd_problem_install(P, []), ( memberchk(det_mode=DetMode, Options) -> true ; DetMode = major_minor ), tptpcd_problem_to_pieform(P, Form, DetMode), ( memberchk(prover9_settings=Settings, Options) -> true ; Settings = [clear(auto_denials), clear(print_given)] ), Options1 = [mace=false, timeout=Timeout, process_output=import_cd:pr9_proof_to_d(D), prover9_settings=Settings, printing=false, r=true, subprover_time=Time], append(Options, Options1, Options2), ppl_valid(Form, Options2), Time1 is round(Time * 1000)/1000.0, format('Proving time:~|~t ~2f~8+ s~n', [Time1]). tptpcd_problem_to_pieform(P, (CD, A -> T), DetMode) :- canonicalize_tptpcd_problem(P, T1, A1), ( DetMode = minor_major -> CD = all([x,y], ( thm(x), thm(x=>y) -> thm(y))) ; CD = all([x,y], ( thm(x=>y), thm(x) -> thm(y))) ), ( \+ ground(T1) -> err('Nonground goal theorem: ~q', [T1]) ; true ), ctp_goal(T1, T), ctp_axioms(A1, A). ctp_goal([~thm(G)], thm(G)). ctp_axioms([[thm(A)]], all(V, thm(A1))) :- !, copy_term(A, A1), term_variables(A1, V), grd_p(V). ctp_axioms([[thm(A)]|Ax], (all(V, thm(A1)), Ax1)) :- copy_term(A, A1), term_variables(A1, V), grd_p(V), ctp_axioms(Ax, Ax1). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% exp(sect(6)-1) :- expinfo('demo of Prover9 in PIE: Syll and Peirce from axiom Łukasiewicz'), requirements([tptp, prover9]), ( member(P, ['LCL082-1', 'LCL083-1']), format('Proving problem ~w with Prover9~n', [P]), tptpcd_prover9_proof(P, 100, D, []), format('Found proof: ~q~n', [D]), fail ; true ). exp(sect(6)-2) :- %% Takes about 30 min (in particular the [naively implemented] %% C-reduction and determining C-regularity.) expinfo('Section 6.2: Prover9\'s proofs and reductions'), requirements([time(1800), tptp, prover9]), ( member(DetMode, [minor_major, major_minor]), format('----------------------------------------'), format('--------------------------------------~n'), format('Det mode ~w~n', [DetMode]), tptpcd_prover9_proof('LCL038-1', 100, D, [det_mode=DetMode]), inspect_prover9_proof(D), fail ; true ). inspect_prover9_proof(D1) :- install_named_axiom(luk, [quiet]), format('---- (1) Given proof:~n'), show_info(D1), format('---- (2) N-simplification of (1):~n'), d_simp_n(D1, D2A), nsols( sub_term(n, D2A), NN), format('Occurrences of n: ~D~n', [NN]), d_n_to_1(D2A, D2), show_info(D2), format('---- (3) S-reduction of (2):~n'), red_xs(D2, D3, NS), format('~NS-reduction steps: ~D', [NS]), show_info(D3), format('---- (4) C-reduction of (2):~n'), red_xc(D2, D4, NC), format('~NC-reduction steps: ~D', [NC]), show_info(D4), format('---- (5) C-reduction of (2):~n'), red_xc(D3, D5, NC5), format('~NC-reduction steps: ~D', [NC5]), show_info(D5). show_info(D) :- show_dims(D), show_rs_rc(D). show_dims(D) :- d_csize(D, CS), d_tsize(D, TS), d_height(D, HS), d_scsize(D, SS), d_max_lemma_tsize(D, FTM), d_max_lemma_height(D, FHM), format('~N~|DC:~t~D~6+; ~|DT:~t~D~11+; ~|DH:~t~D~6+; ~|DX:~t~D~9+', [CS, TS, HS, SS]), format(' ~|FT-Max:~t~D~10+; ~|FH-Max:~t~D~10+~n', [FTM, FHM]). show_rs_rc(D) :- ( d_is_regular(ipt_mgt, D) -> RS = yes ; RS = no ), format('Regularity RS: ~w; RC: ', [RS]), flush_output, ( d_is_regular(red_c, D) -> RC = yes ; RC = no ), format('~w~n', [RC]). d_max_lemma_tsize(D, N) :- install_named_axiom(luk, [quiet]), findall(S, ( sub_term_u(D1,D), d_mgt(D1, F), f_tsize(F, S) ), S1), numbers_maximum(S1, N). d_max_lemma_height(D, N) :- install_named_axiom(luk, [quiet]), findall(S, ( sub_term_u(D1,D), d_mgt(D1, F), f_height(F, S) ), S1), numbers_maximum(S1, N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Naive Implementations of S- and C-Reduction %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% red_xs(D, D1, N) :- info_progress_start, red_xs(D, D1, 0, N). red_xs(D, D1, N, N1) :- info_progress(10, 1), d_red_step_ipt_mgt(D, D2), !, N2 is N+1, red_xs(D2, D1, N2, N1). red_xs(D, D, N, N). d_red_step_ipt_mgt(D, D1) :- d_to_dy(D, DY), dy_red_step_ipt_mgt(DY, DY1), dy_to_d(DY1, D1). dy_red_step_ipt_mgt(DY, DY1) :- DY = d(_,_,Y), dy_to_d(DY, D), sub_term_u(D2, D), D2 \= D, d_mgt(D2, F), subsumes_term(F, Y), !, d_to_dy(D2, DY1). dy_red_step_ipt_mgt(d(A,B,_), d(A1,B,_)) :- dy_red_step_ipt_mgt(A, A1), !. dy_red_step_ipt_mgt(d(A,B,_), d(A,B1,_)) :- dy_red_step_ipt_mgt(B, B1). red_xc(D, D1, N) :- info_progress_start, red_xc(D, D1, 0, N). red_xc(D, D1, N, N1) :- info_progress(10, 1), d_red_step(xc, D, D2), !, N2 is N+1, red_xc(D2, D1, N2, N1). red_xc(D, D, N, N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% Section 6.2: PSP level enumeration and a short proof %%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% %%%% The proof D_{29}, for axiom Łukasiewicz, i.e. a list of the proofs of %%%% Syll, Peirce and Simp. See also %%%% http://cs.christophwernhard.com/cdtools/downloads/cdtools/exp/exp_luk.pl %%%% luk_d29_ds(Ds) :- Ds = [d(d(d(d(1,d(d(d(1,d(d(d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1),1),d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1))),d(1,d(d(d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1),1),d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1)))),1)),1),1),1),d(d(d(d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1),d(1,1)),d(d(d(1,d(1,1)),1),1)),d(1,1)),d(d(d(1,1),d(d(d(1,d(1,1)),1),1)),1)]. gen_d_psp_of_level(0, 1). gen_d_psp_of_level(N, d(A,B)) :- N > 0, N1 is N-1, gen_d_psp_of_level(N1, D), sub_term_u(D1, D), ( A=D, B=D1 ; D\=D1, B=D, A=D1 ). exp(sect(6)-3) :- expinfo('Section 6.2, Definition 52'), ( between(0, 8, I), nsols( gen_d_psp_of_level(I, _), N), format('Cardinality of PSP level ~w:~|~t ~D~12+~n', [I, N]), fail ; true ). exp(sect(6)-4) :- expinfo('finding the short proof of Syll from axiom Łukasiewicz with SGCD'), O = [once=true, gen=inc_psp1, test=[lt_fh(truncate(input*2)+1), lt_ft(truncate(input*3)+1), lt_dup, lt_subs], max_level=1000000, process_news=reg([],[],[])], tptpcd_problem_install('LCL038-1', [goal=Goal]), get_time(T1), sgcd([proof=D, goal=Goal|O]), get_time(T2), T is T2-T1, format('Found poroof: ~q~n', [D]), format('Used time ~2fs~n', [T]), d_csize(D, CS), d_tsize(D, TS), d_height(D, HS), format('Measures - compacted size: ~d, tree size: ~d, height: ~d~n', [CS, TS, HS]). exp(sect(6)-5) :- %% See also: https://arxiv.org/abs/2209.12592, %% https://arxiv.org/abs/2207.08453 expinfo('combinator compression of the short proof of Syll'), requirements([treerepair]), luk_d29_ds([D|_]), d_to_gr(D, G), gr_to_fsk(G, F, [lambda_optim=2, simp=red]), format('------------------------------------------------------------~n'), format('Compressed proof in factorized D-term notation:~n'), pp_sk(F, [fact=1,style=dterm,vstart=2,vhead='',sort=1]), format('------------------------------------------------------------~n'), format('Compressed proof in factorized application notation:~n'), pp_sk(F, [fact=1,style=trad,vstart=2,vhead='',sort=1]).