一句话：通过双标签证明搜索，证明直觉主义模态逻辑 S4 可判定并获得有限模型性质。
本文研究 Fischer Servi 提出的直觉主义模态逻辑 S4 的可判定性。该问题自 1994 年 Simpson 的博士论文中提出后，已悬置近三十年。作者在一个带标签的演绎系统中进行证明搜索，其标签并非只使用一个二元关系，而是同时使用两个关系：一个对应模态逻辑的可达关系，另一个对应直觉主义 Kripke 框架的序关系。该搜索算法对输入公式要么输出证明，要么输出有限反模型。由此，作者不仅证明了直觉主义 S4 的可判定性，还额外建立了该逻辑的有限模型性质，这同样是该领域长期未决的问题。
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson’s PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{GirlandoKMMS23,
title = {Intuitionistic S4 is decidable},
author = {Marianna Girlando and Roman Kuznets and Sonia Marin and Marianela Morales and Lutz Straßburger},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175684}
}