Extending a High-Performance Prover to Higher-Order Logic

This is the package containing raw evaluation data and other related data for the submission
Extending a High-Performance Prover to Higher-Order Logic.

The problems used for the evaluation are stored in the problems/ directory. Higher-order TPTP benchmarks are in TPTP_HO subdirectory, while first-order TPTP benchmarks are in TPTP_FO subdirectory. Sledgehammer benchmarks are stored in SH subdirectory.

Figures 2 and 3 in the submission are automatically created using Python script get_table.py from scripts/ directory. This script processes raw data obtained from StarExec, which is stored in the results/ directory.

To create Figure 2 use the following command:

  python3 scripts/get_table.py results/ scripts/tptp_sh.json

Figure 3 is created using:

  python3 scripts/get_table.py results/ scripts/fo.json

Directory e-26-4 contains both first-order (eprover) and higher-order (eprover-ho)
binaries compiled under Ubuntu 18-04. The directory e-26-4 can be packaged in
an archive and submitted to StarExec for evaluation. starexec_run_as4_serialize.sh
was used on SH benchmarks, starexec_run_as8.sh was used on higher-order TPTP
benchmarks. starexec_run_fo-boa and starexec_run_ho-boa were used on first-order
benchmarks. To run the scripts locally, environment variables STAREXEC_CPU_LIMIT
and STAREXEC_WALLCLOCK_LIMIT must be set. Note these scripts do not limit any resources
of lambdaE and rely on StarExec facilities for this purpose.

lambdaE was compiled from the master_bce_merge, branch of eprover github (https://github.com/eprover/eprover),
with the git commit hash 693e48236d18e6b9a8f60db9ff2c56503ed16945.