-
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ödel-Löb logic GL, for which our formalisation clarifies an important point in an… ▽ More
Submitted 29 April, 2024; v1 submitted 16 February, 2024; originally announced February 2024.
Comments: 18 pages, to appear in IJCAR 2024
MSC Class: 03B45; 03B20; 03F45; 68V20 ACM Class: F.4.1; I.2.3; I.2.4