A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
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_ | 1866909444441374720 |
|---|---|
| author | Wang, Shuai |
| author_facet | Wang, Shuai |
| contents | For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are generally kept relatively small. On top of the kernel, additional symbols and inference rules are defined. This paper presents an analysis of how kernel extension reduces the size of proofs and impacts proof checking. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_20973 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking Wang, Shuai Logic in Computer Science Symbolic Computation 68Q60, 68V30 F.4.1; F.3.1 For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are generally kept relatively small. On top of the kernel, additional symbols and inference rules are defined. This paper presents an analysis of how kernel extension reduces the size of proofs and impacts proof checking. |
| title | A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking |
| topic | Logic in Computer Science Symbolic Computation 68Q60, 68V30 F.4.1; F.3.1 |
| url | https://arxiv.org/abs/2412.20973 |