Experiments with Choice in Dependently-Typed Higher-Order Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910645462499328 |
|---|---|
| author | Ranalter, Daniel Brown, Chad E. Kaliszyk, Cezary |
| author_facet | Ranalter, Daniel Brown, Chad E. Kaliszyk, Cezary |
| contents | Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_08874 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Experiments with Choice in Dependently-Typed Higher-Order Logic Ranalter, Daniel Brown, Chad E. Kaliszyk, Cezary Logic in Computer Science Artificial Intelligence F.4.1; I.2.3 Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching 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. |
| title | Experiments with Choice in Dependently-Typed Higher-Order Logic |
| topic | Logic in Computer Science Artificial Intelligence F.4.1; I.2.3 |
| url | https://arxiv.org/abs/2410.08874 |