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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</a><br>

Návaznosti

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

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

Automated Reasoning

ISBN

978-3-031-63498-7

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

86-104

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Nancy

Datum konání akce

1. 7. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001273489700006