直觉主义模态逻辑 IS4（及 IK4）的一个判定过程
A decision procedure for intuitionistic modal logic IS4 (and IK4)
浏览论文内容
中文总结 AI 辅助
本文为直觉主义模态逻辑 IS4 和 IK4 提供了构造性判定过程，通过引入循环规则证明其可判定性及有限模型性质，并修正了先前工作的错误。
中文摘要 AI 辅助
在本文中，我们证明了两种直觉主义模态逻辑 IS4 和 IK4 是可判定的。我们提供了一个构造性的判定过程，对于给定的公式，该过程要么产生一个证明该公式有效的证明，要么产生一个有限的模型来反驳该公式，从而也证明了这两种逻辑的有限模型性质。我们策略的主要成分是引入（可能不健全的）循环规则，这些规则编码了证明搜索中的重复行为。本文修正了我们之前在 LICS'23 投稿中的一个错误。
英文摘要
In this paper, we show that the two intuitionistic modal logics IS4 and IK4 are decidable. We provide a constructive decision procedure, that, given a formula, produces either a proof showing the formula to be valid or a finite countermodel falsifying the formula, thus also proving the finite model property for both logics. The main ingredient of our strategy is the introduction of (possibly unsound) loop rules, which encode repeating behaviour in proof search. This paper fixes a previous mistake in our LICS'23 contribution.
