Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00380916" target="_blank" >RIV/68407700:21730/24:00380916 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1007/978-3-031-63498-7_6" target="_blank" >https://doi.org/10.1007/978-3-031-63498-7_6</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-63498-7_6" target="_blank" >10.1007/978-3-031-63498-7_6</a>

Result language

angličtina

Original language name

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/LL1902" target="_blank" >LL1902: Powering SMT Solvers by Machine Learning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Automated Reasoning

ISBN

978-3-031-63498-7

ISSN

0302-9743

e-ISSN

1611-3349

Number of pages

19

Pages from-to

86-104

Publisher name

Springer

Place of publication

Cham

Event location

Nancy

Event date

Jul 1, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001273489700006