Mechanised uniform interpolation for modal logics K, GL, and iSL

Autor:	Férée, Hugo, van der Giessen, Iris, van Gool, Sam, Shillito, Ian
Rok vydání:	2024
Předmět:	Computer Science - Logic in Computer Science Mathematics - Logic 03B45 03B20 03F45 68V20 F.4.1 I.2.3 I.2.4
Druh dokumentu:	Working Paper
Popis:	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\"odel-L\"ob logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong L\"ob 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. Comment: 18 pages, to appear in IJCAR 2024
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2402.10494 Zobrazit plný text záznamu View this record from Arxiv