Supplementary artifacts for
Collection of Bash scripts and SWI-Prolog sources to reproduce the described experiments and as starting point for developing related experiments and applications.
Tar file with a directory with 1374 TPTP FO problem files, one for each POI theorem. The axioms are for all problems the same: the clause for condensed detachment and the three axioms that axiomatize classical propositional logic in set.mm. The conjecture is the respective POI theorem.
File size 685 KB, expands into 6 MB
md5sum:
c1d550c62e7429ffc6b27b4c36db8449
Tar file with a directory with 11 subdirectories, each with 1374 TPTP FO problem files, one for each POI theorem. The problems are like those of poi_tptp.tgz except that the axioms are enhanced by lemmas obtained via DAG compression of proof structures generated by SGCD from the axioms. Within each subdirectory the axioms for all problems are the same. The subdirectory names indicate the parameters used to generate the lemmas.
File size 325 MB, expands into 2.7 GB
md5sum:
2cb4f5a16c5ad21738519871ed5f6a21
Tar file with logs and outputs of SGCD runs presented in the paper. The outputs include proofs of POI problems. A contained file sgcd_logs_concordance.pl provides a mapping between Run-IDs in the paper and the IDs (= file basenames) of the log files. There might be slight differences to values shown in the paper, as these logs were obtained with later re-runs that provide better proof output.
Proofs are represented as DC-terms (dc_representation.pl), a special case of FSK-terms (sk_cd.pl, sk_mgt_cd.pl).
Prolog file
with a fact-set predicate that describes the 1374 POI theorems:
poi_theorem(?TheoremId, ?TheoremFormula, ?ProblemId,
?Rating)
TheoremId comes from set.mm. ProblemId is the basename
for the corresponding TPTP problems.
CD proofs found by Prover9 for 306 POI problems.
Proofs are represented as DC-terms (dc_representation.pl), a special case of FSK-terms (sk_cd.pl, sk_mgt_cd.pl).
CD proofs from set.mm for 1297 POI problems. Converted to proofs of the implication form of the theorems with 1,2,3 as only axioms.
Proofs are represented as DC-terms (dc_representation.pl), a special case of FSK-terms (sk_cd.pl, sk_mgt_cd.pl).
File with stored solutions from SGCD runs for re-use in lemma synthesis. The files are gzipped and in SWI-Prolog's Fast Binary Term I/O format. See thgen script thgen_baserun.sh.
File size 886 MB
md5sum:
3d8099cc64543859193c31ba6a67bb4a
Contact: info@christophwernhard.com