Open AccessComplexity of Admissible Rules in the Implication-Negation Fragment of Intuitionistic Logic
Author(s) -
Petr Cintula,
George Metcalfe
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/cll3
Subject(s) - fragment (logic) , negation , set (abstract data type) , intuitionistic logic , negation as failure , mathematics , pspace , computer science , set theory , discrete mathematics , theoretical computer science , autoepistemic logic , algorithm , computational complexity theory , programming language , multimodal logic , description logic , linear logic
The goal of this paper is to study the complexity of the set of admissible rules of the implication-negation fragment of intuitionistic logic IPC. Surprisingly perhaps, although this set strictly contains the set of derivable rules (the fragment is not structurally complete), it is also PSPACE-complete. This differs from the situation in the full logic IPC where the admissible rules form a co-NEXP-complete set.