Complexity of subclasses of the intuitionistic propositional calculus
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.
complexity of the decision problem for subclasses of intuitionistic propositional calculus
scientific article; zbMATH DE number 438468
scientific article