Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL

Hugo Férée; Iris van der Giessen; Sam van Gool; Ian Shillito

doi:10.1007/978-3-031-63501-4_3

Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL

Hugo Férée, Iris van der Giessen, Sam van Gool^*, Ian Shillito

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

113 Downloads (Pure)

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 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.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II
Editors	Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
Publisher	Springer
Chapter	3
Pages	43-60
Number of pages	18
Volume	2
ISBN (Electronic)	9783031635014
ISBN (Print)	9783031635007
DOIs	https://doi.org/10.1007/978-3-031-63501-4_3
Publication status	Published - 2 Jul 2024

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Cham
Volume	14740
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-031-63501-4_3Licence: Creative Commons: Attribution (CC BY)

AutomatedReasoning-LNICS-14740Final published version, 8.96 MBLicence: Creative Commons: Attribution (CC BY)

Structure vs. Invariants in Proofs (StrIP)
Das, A. (Principal Investigator)
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

Férée, H., van der Giessen, I., van Gool, S., & Shillito, I. (2024). Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. In C. Benzmüller, M. J. H. Heule, & R. A. Schmidt (Eds.), Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II (Vol. 2, pp. 43-60). (Lecture Notes in Computer Science; Vol. 14740). Springer. https://doi.org/10.1007/978-3-031-63501-4_3

Férée, Hugo ; van der Giessen, Iris ; van Gool, Sam et al. / Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II. editor / Christoph Benzmüller ; Marijn J. H. Heule ; Renate A. Schmidt. Vol. 2 Springer, 2024. pp. 43-60 (Lecture Notes in Computer Science).

@inproceedings{f5aa8753b50940bba909185230af1fb1,

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.",

author = "Hugo F{\'e}r{\'e}e and {van der Giessen}, Iris and {van Gool}, Sam and Ian Shillito",

year = "2024",

month = jul,

day = "2",

doi = "10.1007/978-3-031-63501-4_3",

language = "English",

isbn = "9783031635007",

volume = "2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "43--60",

editor = "Christoph Benzm{\"u}ller and Heule, {Marijn J. H.} and Schmidt, {Renate A.}",

booktitle = "Automated Reasoning",

}

Férée, H, van der Giessen, I, van Gool, S & Shillito, I 2024, Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. in C Benzmüller, MJH Heule & RA Schmidt (eds), Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II. vol. 2, Lecture Notes in Computer Science, vol. 14740, Springer, pp. 43-60. https://doi.org/10.1007/978-3-031-63501-4_3

Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. / Férée, Hugo; van der Giessen, Iris; van Gool, Sam et al.
Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II. ed. / Christoph Benzmüller; Marijn J. H. Heule; Renate A. Schmidt. Vol. 2 Springer, 2024. p. 43-60 (Lecture Notes in Computer Science; Vol. 14740).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL

AU - Férée, Hugo

AU - van der Giessen, Iris

AU - van Gool, Sam

AU - Shillito, Ian

PY - 2024/7/2

Y1 - 2024/7/2

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.

U2 - 10.1007/978-3-031-63501-4_3

DO - 10.1007/978-3-031-63501-4_3

M3 - Conference contribution

SN - 9783031635007

VL - 2

T3 - Lecture Notes in Computer Science

SP - 43

EP - 60

BT - Automated Reasoning

A2 - Benzmüller, Christoph

A2 - Heule, Marijn J. H.

A2 - Schmidt, Renate A.

PB - Springer

ER -

Férée H, van der Giessen I, van Gool S, Shillito I. Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. In Benzmüller C, Heule MJH, Schmidt RA, editors, Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II. Vol. 2. Springer. 2024. p. 43-60. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-63501-4_3

Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL

Abstract

Publication series

Access to Document

Fingerprint

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this