An AC complete model checking problem for intuitionistic logic

被引：4
|
作者：
Mundhenk, Martin [1 ]
Wei, Felix [1 ]
机构：
[1] Univ Jena, Inst Informat, D-07737 Jena, Germany
来源：
COMPUTATIONAL COMPLEXITY | 2014年 / 23卷 / 04期
关键词：
Complexity; intuitionistic logic; model checking; AC(1); Heyting algebra;
D O I：
10.1007/s00037-013-0062-z
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We show that the model checking problem for intuitionistic propositional logic with one variable is complete for logspace-uniform AC (1). For superintuitionistic logics with one variable, we obtain NC (1)-completeness for the model checking problem.
引用
收藏
页码：637 / 669
页数：33
相关论文
共 50 条
  • [1] An AC1-complete model checking problem for intuitionistic logic
    Martin Mundhenk
    Felix Wei
    [J]. computational complexity, 2014, 23 : 637 - 669
  • [2] The model checking problem for propositional intuitionistic logic with one variable is AC1-complete
    Mundhenk, Martin
    Weiss, Felix
    [J]. 28TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2011), 2011, 9 : 368 - 379
  • [3] Quantum computation tree logic - Model checking and complete calculus
    Baltazar, P.
    Chadha, R.
    Mateus, P.
    [J]. INTERNATIONAL JOURNAL OF QUANTUM INFORMATION, 2008, 6 (02) : 219 - 236
  • [4] A strongly complete axiomatization of intuitionistic temporal logic
    Chopoghloo, Somayeh
    Moniri, Morteza
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2021, 31 (07) : 1640 - 1659
  • [5] MODEL THEORY FOR INTUITIONISTIC LOGIC
    GABBAY, DM
    [J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1972, 18 (01): : 49 - &
  • [6] MODEL THEORY FOR AN INTUITIONISTIC LOGIC
    RAUSZER, C
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (03) : 459 - 460
  • [7] INFINITY-REGULAR TEMPORAL LOGIC AND ITS MODEL CHECKING PROBLEM
    HAMAGUCHI, K
    HIRAISHI, H
    YAJIMA, S
    [J]. THEORETICAL COMPUTER SCIENCE, 1992, 103 (02) : 191 - 204
  • [8] INTUITIONISTIC IMPLICATION MAKES MODEL CHECKING HARD
    Mundhenk, Martin
    Weiss, Felix
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (02)
  • [9] Temporal logic and model checking
    McMillan, KL
    [J]. VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 36 - 54
  • [10] Model Checking of Spatial Logic
    Li, Tengfei
    Liu, Jing
    Kang, JieXiang
    Sun, Haiying
    Chen, Xiaohong
    Han, Li
    [J]. 2020 27TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2020), 2020, : 169 - 177
12345