The Embedding Path Order for Lambda-Free Higher-Order Terms — Supplementary Material

This page contains supplementary material for the article The Embedding Path Order for Lambda-Free Higher-Order Terms.

Zipperposition

Compilation instructions for Zipperposition, in particular instructions for compilation for StarExec, can also be found in the Zipperposition readme. I used OCaml 4.07.0, branch lfzip, commit 2d9af0d3d1f3501aec8c2988ab8395b1e1ee98ae

Problems

I used the following TPTP (v7.2.0) problems for the evaluation:  TPTP problem list. This lists contains all higher-order (THF) problems, excluding those that contain arithmetic, tuples, the $distinct predicate, or the $ite symbol, as well as those whose clausal normal form generated by Zipperposition is outside the lambda-free fragment. To find those problems, I 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 the calculus is 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

I 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:

EPO
./zipperposition.exe --mode lambda-free-intensional --ord epo

RPO
./zipperposition.exe --mode lambda-free-intensional --ord rpo6

KBO
./zipperposition.exe --mode lambda-free-intensional --ord kbo

appRPO
./zipperposition.exe --mode fo-complete-basic --app-encode intensional --ord rpo6

appKBO
./zipperposition.exe --mode fo-complete-basic --app-encode intensional --ord kbo

As additional command line arguments, I provided the problem's filename, the extension operator (--default-symbol-status lengthlexicographic or --default-symbol-status lengthlexicographicrtl) and the options --stats --profile. On Starexec, I chose a wallclock timeout of 600s, a CPU timeout of 300s. StarExec's machine specifications are:

# Starexec stats nodes 001 - 192:
Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz (2393 MHZ)
10240 KB Cache
263932744 kB main memory

# Software:
OS: CentOS Linux release 7.7.1908 (Core)
kernel: 3.10.0-1062.4.3.el7.x86_64
glibc: glibc-2.17-292.el7.x86_64
gcc-4.8.5-39.el7.x86_64
glibc-2.17-292.el7.i686

Results

Get an interactive overview of the results here: Interactive evaluation results

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

Counter-example generation with Lazy SmallCheck

Some of the examples in the paper were generated using Lazy SmallCheck. Here are the programs used to this: Counter-example generation

Formalization

Proofs of the properties of EPO were formalized in Isabelle/HOL and published in the Archive of Formal Proofs: Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms