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 Term