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

2010/12/17 by Martin Mundhenk, Mundhenk, Martin, Felix Weiß +2
Computer Science · Economics, Econometrics and Finance · #03B20 (Secondary) #68Q17 (Primary) #Computational Complexity (cs.CC) #F.2 #F.4 #FOS: Computer and information sciences #Formal Methods in Verification #Game Theory and Voting Systems #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1012.3828

openalex publication_date 2010/12/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We show that the model checking problem for intuitionistic propositional\nlogic with one variable is complete for logspace-uniform AC1. As basic tool we\nuse the connection between intuitionistic logic and Heyting algebra, and\ninvestigate its complexity theoretical aspects. For superintuitionistic logics\nwith one variable, we obtain NC1-completeness for the model checking problem.\n

Related

• Complexity of the Model Checking problem for inquisitive propositional and modal logic
• On the complexity of the model checking problem
• Dichotomies and Duality in First-order Model Checking Problems
• Parameterised Complexity of Propositional Inclusion and Independence Logic
• Fixed-parameter tractability, definability, and model checking