A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking

TL;DR

This paper analyzes how extending the kernel of Interactive Theorem Provers affects proof size and checking, highlighting implications for reliability and efficiency.

Contribution

It provides a qualitative analysis of kernel extension effects on proof reduction and proof checking in ITPs, an area with limited prior focus.

Findings

Kernel extension reduces proof size

Impacts proof checking process

Affects reliability of ITPs

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.