DOI: 10.5281/zenodo.3992618
title: Superposition for Lambda-Free Higher-Order Logic — Supplementary Material for the Journal Article

description: We provide the following supplementary material for our article. <strong>Zipperposition</strong> 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 <code>lmcs2020</code>, commit 2031e216c1941acd76187882a073e8f1e53383f2 <strong>Problems</strong> 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 <code>(@@+)</code>, <code>(@@-)</code>, <code>(@+)</code>, <code>(@-)</code>, <code>(&)</code>, or tuples, as well as the <code>SYN000</code> 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 <strong>Run scripts</strong> 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:<br> <code>./zipperposition.exe --mode=fo-complete-basic</code> Applicative encoding mode (intensional):<br> <code>./zipperposition.exe --mode=fo-complete-basic --app-encode=intensional</code> Applicative encoding mode (extensional):<br> <code>./zipperposition.exe --mode=fo-complete-basic --app-encode=extensional</code> Nonpurifying intensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-intensional</code> Nonpurifying extensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-extensional</code> Purifying intensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-purify-intensional</code> Purifying extensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-purify-extensional</code> As additional command line arguments, we provided the problem's filename, the order (<code>--ord=lambdafree_rpo</code> or <code>--ord lambdafree_kbo</code> or <code>--ord epo</code>), and the following parameters for heuristics that were obtained by optimizing the first-order mode in preliminary experiments: <pre>--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 </pre> 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: <pre>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 </pre> <strong>Results</strong> 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 <strong>Examples</strong> 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