A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
Logic in Computer Science
2024-12-31 v1 Symbolic Computation
Abstract
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.
Keywords
Cite
@article{arxiv.2412.20973,
title = {A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking},
author = {Shuai Wang},
journal= {arXiv preprint arXiv:2412.20973},
year = {2024}
}
Comments
The paper was presented in the student session of the European Summer School in Logic, Language, and Information (ESSLLI) in 2016