Towards a Coq formalization of a quantified modal logic

Abstract

We present a Coq formalization of the Quantified Reflection Calculus with one modality, or ${\mathsf{QRC}}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of ${\mathsf{QRC}}_1$ in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalization of the soundness theorem. We focus on the design decisions inherent to the formalization and the insights that led to new and simplified proofs.

To appear in the proceedings for ARQNL 2022. See https://zenodo.org/record/6615336 for the associated Coq code

Cited by in corpus (1)

• UTC Time, Formally Verified