The model checking problem for intuitionistic propositional logic with one variable is AC1-complete
Preprint
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
All Related Versions
This publication has 11 references indexed in Scilit:
- On the polynomial-space completeness of intuitionistic propositional logicArchive for Mathematical Logic, 2003
- Circuits, Matrices, and Nonassociative ComputationJournal of Computer and System Sciences, 1995
- A taxonomy of problems with fast parallel algorithmsInformation and Control, 1985
- On uniform circuit complexity1979
- Intuitionistic propositional logic is polynomial-space completeTheoretical Computer Science, 1979
- Implicational formulas in intuitionistic logicThe Journal of Symbolic Logic, 1974
- Characterizations of Pushdown Machines in Terms of Time-Bounded ComputersJournal of the ACM, 1971
- There are infinitely many Diodorean modal functionsThe Journal of Symbolic Logic, 1966
- On formulas of one variable in intuitionistic propositional calculusThe Journal of Symbolic Logic, 1960
- Modal Logics Between S 4 and S 5Mathematical Logic Quarterly, 1959