@inproceedings{17f786af17a44491a81753f09dabdf20,
title = "Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL",
abstract = "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{\"o}del-L{\"o}b logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong L{\"o}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.",
keywords = "formal verification, proof theory, propositional quantifiers, provability logic, uniform interpolation",
author = "Hugo F{\'e}r{\'e}e and Giessen, \{Iris van der\} and Gool, \{Sam van\} and Ian Shillito",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.; 12th International Joint Conference on Automated Reasoning, IJCAR 2024 ; Conference date: 03-07-2024 Through 06-07-2024",
year = "2024",
doi = "10.1007/978-3-031-63501-4\_3",
language = "English",
isbn = "9783031635007",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science+Business Media B.V.",
pages = "43--60",
editor = "Christoph Benzm{\"u}ller and Heule, \{Marijn J. H.\} and Schmidt, \{Renate A.\}",
booktitle = "Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings",
address = "Netherlands",
}