| ||||
| ||||
![]() Title:Towards a Coq Formalization of a Quantified Modal Logic Authors:Ana de Almeida Borges Conference:ARQNL 2022 Tags:Coq, feasible fragments, formalization, Kripke semantics, modal logic and strictly positive logic Abstract: We present a Coq formalization of the Quantified Reflection Calculus with one modality, or QRC1. 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 QRC1 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. Towards a Coq Formalization of a Quantified Modal Logic ![]() Towards a Coq Formalization of a Quantified Modal Logic | ||||
Copyright © 2002 – 2025 EasyChair |