Superposition for Lambda-Free Higher-Order Logic — Supplementary Material for the Journal Article

We provide the following supplementary material for our article. Zipperposition Compilation instructions for Zipperposition, in particular instructions for compilation for StarExec, can also be found in the Zipperposition readme. We used OCaml 4.07.0, branch lmcs2020, commit 2031e216c1941acd76187882a073e8f1e53383f2 Problems We used the following first-order (TFF) and the higher-order (THF) TPTP (v7.3.0) problems for the evaluation: TFF problem list  THF problem list. These lists were obtained by excluding all problems that contain arithmetic, the symbols (@@+), (@@-), (@+), (@-), (&), or tuples, as well as the SYN000 problems, which are only intended to test the parser, and problems whose clausal normal form takes longer than 15s to compute or falls outside the lambda-free fragment. The following archive contains instructions on how the benchmarks were selected: Benchmark selection Note that Zipperposition is not aware that our calculi are complete for this fragment and it will always report "GaveUp" instead of "CounterSatisfiable" if the calculus saturates. The selection of TPTP problems and the problems generated by Isabelle/Sledgehammer can be downloaded here: Benchmarks Run scripts We used the following run scripts on StarExec. This archive also contains the Zipperposition binary, compiled for StarExec: StarExec run scripts The scripts use the following command-line options for Zipperposition First-order mode: ./zipperposition.exe --mode=fo-complete-basic Applicative encoding mode (intensional): ./zipperposition.exe --mode=fo-complete-basic --app-encode=intensional Applicative encoding mode (extensional): ./zipperposition.exe --mode=fo-complete-basic --app-encode=extensional Nonpurifying intensional calculus: ./zipperposition.exe --mode=lambda-free-intensional Nonpurifying extensional calculus: ./zipperposition.exe --mode=lambda-free-extensional Purifying intensional calculus: ./zipperposition.exe --mode=lambda-free-purify-intensional Purifying extensional calculus: ./zipperposition.exe --mode=lambda-free-purify-extensional As additional command line arguments, we provided the problem's filename, the order (--ord=lambdafree_rpo or --ord lambdafree_kbo or --ord epo), and the following parameters for heuristics that were obtained by optimizing the first-order mode in preliminary experiments: --kbo-weight-fun=modarity \ -q "7|prefer-sos|pnrefined(2,1,1,1,2,2,2)" \ -q "4|prefer-short-trail|pnrefined(1,1,1,2,2,2,0.5)" \ -q "1|prefer-processed|fifo" \ -q "7|prefer-ground|conjecture-relative-var(1,l,f)" \ -q "6|prefer-goals|conjecture-relative-var(1,s,f)" \ --select=e-selection7 On Starexec, we chose a wallclock timeout of 360 s, a CPU timeout of 180 s, and a memory limit of 128 GB. StarExec's machine specifications are: Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz (2393 MHZ) 10240 KB Cache 263932744 kB main memory OS: CentOS Linux release 7.7.1908 (Core) kernel: 3.10.0-1062.4.3.el7.x86_64 Results Download the raw output of the evaluation and the .csv files created by StarExec here: Raw evaluation output TFF Raw evaluation output SH256 Raw evaluation output SH16 Raw evaluation output THF Evaluation results as CSV file + script to compile the statistics Examples We tested the examples given in our paper in Zipperposition. Here are the problem files we used. Some are in TPTP format (.p) and some are in Zipperposition format (.zf). Example 3.3 Example 3.4 Example 3.5 Example 3.6 Example 3.7