Intuitionistic implication makes model checking hard

DOI10.2168/LMCS-8(2:3)2012MaRDI QIDQ2887060zbMATH OpenOpenAlexFDO

Authors Martin Mundhenk, Felix Weiss

Publication date 16 May 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1107.1963

zbMATH Keywords

complexityintuitionistic logicmodel checkingP-completeness

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Modal logic (including the logic of norms) (03B45) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

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

Recommendations

• The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions
• Model-Checking Problems as a Basis for Parameterized Intractability
• Proof complexity of intuitionistic implicational formulas
• Model checking for modal intuitionistic dependence logic
• scientific article; zbMATH DE number 1705163
• Implication-Based Approximating Bounded Model Checking
• scientific article; zbMATH DE number 1834576
• A proof theory for model checking
• An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic
• On the complexity of the model checking problem

Cited in

(3)

• The complexity of primal logic with disjunction
• The model checking problem for propositional intuitionistic logic with one variable is \(\text{AC}^1\)-complete
• An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic

This page was built for publication: Intuitionistic implication makes model checking hard

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2887060)