论文标题
迈向量化模态逻辑的COQ形式化
Towards a Coq formalization of a quantified modal logic
论文作者
论文摘要
我们提出了一种具有一种模态的量化反射计算的COQ形式化，或$ \ Mathsf {qrc} _1 $。这是先前研究其在证明理论中的应用的可决定性，严格阳性和量化的模态逻辑。亮点是$ \ mathsf {qrc} _1 $的深层嵌入，在Coq证明助手中，Kripke模型的机械化具有不同的域和声音定理的形式化。我们专注于形式化固有的设计决策以及导致新的和简化的证据的见解。
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.
