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