The model checking problem for intuitionistic propositional logic with one variable is AC1-complete
Martin Mundhenk, Felix Weiß · arXiv (Cornell University) · 2010
We show that the model checking problem for intuitionistic propositional logic with one variable is complete for logspace-uniform AC1. As basic tool we use the connection between intuitionistic logic and Heyting algebra, and investigate its complexity theoretical aspects. For superintuitionistic logics with one variable, we obtain NC1-completeness for the model checking problem.