Superposition for Lambda-Free Higher-Order Logic
Supplementary Material for the journal article

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann

We provide the following supplementary material for our article.

Evaluation Setup

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 a000340e47a56b7dc7e42eff768a29447807516d

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, tuples, choice, the $distinct predicate, the $ite symbol, or the (∧) symbol, as well as problems whose clausal normal form generated by Zipperposition is outside the lambda-free fragment. To check the latter, we used a program that can be found under zipperposition/_build/default/src/tools/type_check.exe after compiling Zipperposition. Note that the lambda-free mode of Zipperposition itself will not check whether the problem is in the fragment or not. It is neither 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

As additional command line arguments, we provided the problem's filename and the order (--ord=lambdafree_rpo or --ord lambdafree_kbo or --ord epo). 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:

  CPU Model name: Intel(R) Xeon(R) CPU E5-2667 v4 0 @ 3.20GHz
  OS:             CentOS Linux release 7.4.1708 (Core) 
  kernel:         3.10.0-957.12.2.el7.x86_64

Results

Download the raw output of the evaluation and the .csv files created by StarExec here:

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).