An AC^1-complete model checking problem for intuitionistic logic

DOI10.1007/S00037-013-0062-ZzbMATH OpenNoneOpenAlexW2072923153MaRDI QIDQ475340FDOQ475340

Authors: Martin Mundhenk, Felix Wei 

Publication date: 26 November 2014

Published in: Computational Complexity (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00037-013-0062-z

Recommendations

• The model checking problem for propositional intuitionistic logic with one variable is \(\text{AC}^1\)-complete
• The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions
• Intuitionistic implication makes model checking hard
• Computer Science Logic
• scientific article; zbMATH DE number 2209833

zbMATH Keywords

complexitymodel checkingintuitionistic logicHeyting algebra\(\mathsf{AC}^{1}\)

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Subsystems of classical logic (including intuitionistic logic) (03B20) Heyting algebras (lattice-theoretic aspects) (06D20)

Cites Work

• Title not available (Why is that?)
• On uniform circuit complexity
• A taxonomy of problems with fast parallel algorithms
• Semantical investigations in Heyting's intuitionistic logic
• Alternation
• On closed elements in closure algebras
• Intuitionistic implication without disjunction
• An Optimal Parallel Algorithm for Formula Evaluation
• Intuitionistic propositional logic is polynomial-space complete
• A short introduction to intuitionistic logic
• Characterizations of Pushdown Machines in Terms of Time-Bounded Computers
• Logic and structure
• On formulas of one variable in intuitionistic propositional calculus
• Modal Logics Between S 4 and S 5
• On the polynomial-space completeness of intuitionistic propositional logic
• Circuits, matrices, and nonassociative computation
• Intuitionism. An introduction. 3rd revised ed
• Intuitionistic implication makes model checking hard
• The model checking problem for propositional intuitionistic logic with one variable is \(\text{AC}^1\)-complete
• Complexity of intuitionistic and Visser's basic and formal logics in finitely many variables
• The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions
• Implicational formulas in intuitionistic logic
• On the Tape Complexity of Deterministic Context-Free Languages
• There are infinitely many Diodorean modal functions

Cited In (6)

• Intuitionistic implication makes model checking hard
• The complexity of primal logic with disjunction
• The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions
• Term Rewriting and Applications
• The model checking problem for propositional intuitionistic logic with one variable is \(\text{AC}^1\)-complete
• The model checking fingerprints of CTL operators

This page was built for publication: An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q475340)