The model checking problem for propositional intuitionistic logic with one variable is AC^1-complete

Martin Mundhenk & Felix Weiß
We investigate the complexity of the model checking problem for propositional intuitionistic logic. We show that the model checking problem for intuitionistic logic with one variable is complete for logspace-uniform AC^1, and for intuitionistic logic with two variables it is P-complete. For superintuitionistic logics with one variable, we obtain NC^1-completeness for the model checking problem and for the tautology problem.