Experiments with Choice 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%3A00381417" target="_blank" >RIV/68407700:21730/24:00381417 - isvavai.cz</a>

Result on the web

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

Result language

angličtina

Original language name

Experiments with Choice in Dependently-Typed Higher-Order Logic

Original language description

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.

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

LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Number of pages

10

Pages from-to

311-320

Publisher name

EasyChair Publications

Place of publication

Manchester

Event location

Balaclava

Event date

May 26, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—