DHOL version of Lash
Home
Contents
description source code experiments

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.