Experiments with Choice in Dependently-Typed Higher-Order Logic
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00381417" target="_blank" >RIV/68407700:21730/24:00381417 - isvavai.cz</a>
Výsledek na webu
<a href="https://doi.org/10.29007/2v8h" target="_blank" >https://doi.org/10.29007/2v8h</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.29007/2v8h" target="_blank" >10.29007/2v8h</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Experiments with Choice in Dependently-Typed Higher-Order Logic
Popis výsledku v původním jazyce
Recently an extension to higher-order logic — called DHOL — was introduced, enrich ing the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert’s indefinite choice operator ϵ, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.
Název v anglickém jazyce
Experiments with Choice in Dependently-Typed Higher-Order Logic
Popis výsledku anglicky
Recently an extension to higher-order logic — called DHOL — was introduced, enrich ing the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert’s indefinite choice operator ϵ, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.
Klasifikace
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)
Návaznosti výsledku
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)
Ostatní
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
ISBN
—
ISSN
2398-7340
e-ISSN
2398-7340
Počet stran výsledku
10
Strana od-do
311-320
Název nakladatele
EasyChair Publications
Místo vydání
Manchester
Místo konání akce
Balaclava
Datum konání akce
26. 5. 2024
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—