Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)

TL;DR

This paper introduces a tableaux-based automated reasoning system for a dependently-typed higher-order logic (DHOL), demonstrating its effectiveness and superior performance over traditional HOL provers through implementation and experiments.

Contribution

It presents the first native tableaux calculus for DHOL, integrating automated type checking and outperforming existing HOL provers on DHOL problems.

Findings

DHOL version of Lash outperforms major HOL provers.

The system is sound and complete for DHOL.

Direct reasoning in DHOL improves performance over translation-based methods.

Abstract

Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with PVS being a notable exception. In this paper, we present native rules for automated reasoning in a dependently-typed version (DHOL) of classical higher-order logic (HOL). DHOL has an extensional type theory with an undecidable type checking problem which contains theorem proving. We implemented the inference rules as well as an automatic type checking mode in Lash, a fork of Satallax, the leading tableaux-based prover for HOL. Our method is sound and complete with respect to provability in DHOL. Completeness is guaranteed by the incorporation of a sound and complete translation from DHOL to HOL recently proposed by Rothgang et al. While this translation can already be used as a preprocessing step to any HOL prover, to achieve better performance, our system directly works in DHOL. Moreover, experimental results show that the DHOL version of Lash can outperform all major HOL provers executed on the translation.