Extending a High-Performance Prover to Higher-Order Logic

This is the package containing raw evaluation data and other related data for the submission<br> 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)<br> binaries compiled under Ubuntu 18-04. The directory e-26-4 can be packaged in<br> an archive and submitted to StarExec for evaluation. starexec_run_as4_serialize.sh<br> was used on SH benchmarks, starexec_run_as8.sh was used on higher-order TPTP<br> benchmarks. starexec_run_fo-boa and starexec_run_ho-boa were used on first-order<br> benchmarks. To run the scripts locally, environment variables STAREXEC_CPU_LIMIT<br> and STAREXEC_WALLCLOCK_LIMIT must be set. Note these scripts do not limit any resources<br> 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),<br> with the git commit hash 693e48236d18e6b9a8f60db9ff2c56503ed16945.