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. <strong>Zipperposition</strong> 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 <code>lfzip</code>, commit 2d9af0d3d1f3501aec8c2988ab8395b1e1ee98ae <strong>Problems</strong> 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 <code>$distinct</code> predicate, or the <code>$ite</code> 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 <code>zipperposition/_build/default/src/tools/type_check.exe</code> 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 <strong>Run scripts</strong> 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<br> <code>./zipperposition.exe --mode lambda-free-intensional --ord epo</code> RPO<br> <code>./zipperposition.exe --mode lambda-free-intensional --ord rpo6</code> KBO<br> <code>./zipperposition.exe --mode lambda-free-intensional --ord kbo</code> appRPO<br> <code>./zipperposition.exe --mode fo-complete-basic --app-encode intensional --ord rpo6</code> appKBO<br> <code>./zipperposition.exe --mode fo-complete-basic --app-encode intensional --ord kbo</code> As additional command line arguments, I provided the problem's filename, the extension operator (<code>--default-symbol-status lengthlexicographic</code> or <code>--default-symbol-status lengthlexicographicrtl</code>) and the options <code>--stats --profile</code>. On Starexec, I chose a wallclock timeout of 600s, a CPU timeout of 300s. StarExec's machine specifications are: <pre># 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 </pre> <strong>Results</strong> 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 <strong>Formalization</strong> 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