A general proof certification framework for modal logic

TL;DR

This paper introduces a flexible, modular framework for proof certification in modal logic, leveraging a common kernel and specification language to verify proofs from various theorem provers and formalisms.

Contribution

It presents a general, extensible proof certification framework based on a classical focused sequent calculus, adaptable to multiple modal proof systems and implemented in a Prolog-like language.

Findings

Framework successfully verifies modal proofs in logic K

Modular design allows easy adaptation to different proof formalisms

Implementation demonstrates practical applicability and extensibility

Abstract

One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labeled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.