Complexity of subclasses of the intuitionistic propositional calculus (Q688732)

The author investigates the complexity of the decision problem for subclasses of intuitionistic propositional calculus (IPC) determined by syntactic restrictions, and presents upper bounds for decision procedures locating these subclasses into a lower complexity class like co-NP or polynomial time. His subclasses of IPC are defined in terms of the normal form \(X\Rightarrow g\), where \(g\) is a propositional variable and \(X\) is a list of the formulas of the form \(^ \sim p\), \(p\), \((p\Rightarrow q)\), \(p\Rightarrow(q\Rightarrow r)\), \((p\Rightarrow q)\Rightarrow r\), \(p\Rightarrow(q\lor r)\), \(p\Rightarrow ^ \sim q\), \(^ \sim q\Rightarrow p\), where \(p\), \(q\), \(r\) are variables.