The model checking problem for intuitionistic propositional logic with one variable is AC1-complete

TL;DR

This paper establishes the computational complexity of the model checking problem for intuitionistic propositional logic with one variable, showing it is AC1-complete, and extends results to superintuitionistic logics with NC1-completeness.

Contribution

It proves the AC1-completeness of model checking for intuitionistic logic with one variable and explores complexity for superintuitionistic logics, linking logic and algebraic structures.

Findings

Model checking for intuitionistic logic with one variable is AC1-complete.

Superintuitionistic logics with one variable have NC1-complete model checking.

Uses Heyting algebra to analyze complexity aspects.

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.