Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909248181501952 |
|---|---|
| author | Traversié, Thomas |
| author_facet | Traversié, Thomas |
| contents | Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for theories encoded in higher-order logic in the lambdaPi-calculus modulo theory, a logical framework that extends lambda-calculus with dependent types and user-defined rewrite rules. We develop a tool that implements Kuroda's translation for proofs written in Dedukti, a proof language based on the lambdaPi-calculus modulo theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_06626 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti Traversié, Thomas Logic in Computer Science Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for theories encoded in higher-order logic in the lambdaPi-calculus modulo theory, a logical framework that extends lambda-calculus with dependent types and user-defined rewrite rules. We develop a tool that implements Kuroda's translation for proofs written in Dedukti, a proof language based on the lambdaPi-calculus modulo theory. |
| title | Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.06626 |