Extending a High-Performance Prover to Higher-Order Logic
Description
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-23-3 contains both first-order (eprover) and higher-order (eprover-ho) binaries compiled under Ubuntu 18-04. The directory e-23-3 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 FO 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 wip-bce branch of eprover github (https://github.com/eprover/eprover), with the git commit hash 88509bacca22c28f46bfe0890e3d4c8768bd6568.
Resources
| Name |
Format |
Description |
Link |
|
0 |
|
http://data.europa.eu/88u/dataset/oai-zenodo-org-6389849 |
|
0 |
|
http://data.europa.eu/88u/dataset/oai-zenodo-org-6389849 |