The model checking problem for intuitionistic propositional logic with one variable is AC1-complete
Computational Complexity
2011-09-16 v3 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1012.3828,
title = {The model checking problem for intuitionistic propositional logic with one variable is AC1-complete},
author = {Martin Mundhenk and Felix Weiss},
journal= {arXiv preprint arXiv:1012.3828},
year = {2011}
}
Comments
A preliminary version of this work was presented at STACS 2011. 19 pages, 3 figures