The complexity of disjunction in intuitionistic logic
Journal of Logic and Computation(2020)
摘要
Abstract We study procedures for the derivability problem of fragments of intuitionistic logic. Intuitionistic logic is known to be PSPACE-complete, with implication being one of the main contributors to this complexity. In fact, with just implication alone, we still have a PSPACE-complete logic. We study fragments of intuitionistic logic with restricted implication and develop algorithms for these fragments which are based on the proof rules. We identify a core fragment whose derivability is solvable in linear time. Adding disjunction elimination to this core gives a logic which is solvable in co-NP. These sub-procedures are applicable to a wide variety of logics with rules of a similar flavour. We also show that we cannot do better than co-NP whenever disjunction elimination interacts with other rules.
更多查看译文
关键词
disjunction,logic,complexity
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要