直觉隐含使模型检验困难
Intuitionistic implication makes model checking hard
摘要：
研究了传递Kripke模型上直觉命题逻辑和模态命题逻辑的模型检验问题的复杂性。更具体地说，我们考虑直觉逻辑IPC，基本命题逻辑BPL，形式命题逻辑FPL和Jankov逻辑KC。我们证明了所有这些直觉逻辑的蕴涵片段的模型检验问题是P-完全的。对于BPL和FPL，我们甚至在只有一个变量的蕴涵片段上也达到了P-困难。对于它们的模态同伴的严格蕴涵片段，得到了相同的硬度结果。此外，我们调查是否公式较少的变量和额外的连接使模型检验更容易。而对于蕴涵片段之外的无变量公式，FPL模型检验被证明是在LOGCFL中，问题仍然是BPL的P-完全。
英文摘要：
We investigate the complexity of the model checking problem for intuitionistic and modal propositional logics over transitive Kripke models. More specific, we consider intuitionistic logic IPC, basic propositional logic BPL, formal propositional logic FPL, and Jankov's logic KC. We show that the model checking problem is P-complete for the implicational fragments of all these intuitionistic logics. For BPL and FPL we reach P-hardness even on the implicational fragment with only one variable. The same hardness results are obtained for the strictly implicational fragments of their modal companions. Moreover, we investigate whether formulas with less variables and additional connectives make model checking easier. Whereas for variable free formulas outside of the implicational fragment, FPL model checking is shown to be in LOGCFL, the problem remains P-complete for BPL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
