# Towards a Coq formalization of a quantified modal logic

arXiv: https://arxiv.org/abs/2206.03358 · HTML: https://mlsanity.com/paper/2206.03358/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jun 2022.

## Built on by (most cited first, 1 of 1)

- [VEL: A Formally Verified Reasoner for OWL2 EL Profile](https://mlsanity.com/paper/2412.08739/) (2024)

## Abstract (arXiv)

We present a Coq formalization of the Quantified Reflection Calculus with one modality, or mathsfQRC1. 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 mathsfQRC1 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.