Description
This website hosts accompanying material for the paper
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order-Logic
by J. Niederhauser, C. Brown and C. Kaliszyk which has
been published at IJCAR 2024. The original version of Lash can be found
here.
Source code
You can download the source code including problem files and scripts
for reproducing the experimental results
here.
Experiments
We investigated a set of 34 TPTP DHOL problems which together prove that
list reversal is an involution on dependently-typed lists. The results compare
the performance of Lash in a DHOL-only mode with Lash in an erasure-only mode as
well as all other HOL provers available on SystemOnTPTP on the translated problems.
-
results for the DHOL-only mode of Lash
-
results for the erasure-only mode of Lash
-
results for available HOL provers on SystemOnTPTP