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

DOI10.1007/S00037-013-0062-ZMaRDI QIDQ475340zbMATHOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(6)

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

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)