TY - GEN
T1 - Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL
AU - Férée, Hugo
AU - Giessen, Iris van der
AU - Gool, Sam van
AU - Shillito, Ian
N1 - Publisher Copyright:
© The Author(s) 2024.
PY - 2024
Y1 - 2024
N2 - The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Löb logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.
AB - The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Löb logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.
KW - formal verification
KW - proof theory
KW - propositional quantifiers
KW - provability logic
KW - uniform interpolation
UR - http://www.scopus.com/inward/record.url?scp=85200227291&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-63501-4_3
DO - 10.1007/978-3-031-63501-4_3
M3 - Conference contribution
AN - SCOPUS:85200227291
SN - 9783031635007
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 43
EP - 60
BT - Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings
A2 - Benzmüller, Christoph
A2 - Heule, Marijn J. H.
A2 - Schmidt, Renate A.
PB - Springer Science and Business Media Deutschland GmbH
T2 - 12th International Joint Conference on Automated Reasoning, IJCAR 2024
Y2 - 3 July 2024 through 6 July 2024
ER -