VEL is a Coq-verified EL++ subsumption reasoner with extracted OCaml code; the formalization found two errors in Baader et al.'s completeness proof and fixed them with an A-extension and a strengthened lemma.
Towards a Coq formalization of a quantified modal logic
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
fields
cs.LO 1years
2024 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
VEL: A Formally Verified Reasoner for OWL2 EL Profile
VEL is a Coq-verified EL++ subsumption reasoner with extracted OCaml code; the formalization found two errors in Baader et al.'s completeness proof and fixed them with an A-extension and a strengthened lemma.