IK is the IK-bisimulation-invariant fragment of intuitionistic first-order logic, accompanied by a Hennessy-Milner theorem and intuitionistic analogues of Los's theorem, elementary embeddings, and countable saturation.
de Paiva (2003): Natural deduction and context as (constructive) modality
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
years
2026 2verdicts
UNVERDICTED 2representative citing papers
Introduces constructive neighbourhood semantics and an adapted structured calculus for intuitionistic monotone modal logic IM, proving decidability and noting analogies to classical variants of M and K.
citing papers explorer
-
Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic
IK is the IK-bisimulation-invariant fragment of intuitionistic first-order logic, accompanied by a Hennessy-Milner theorem and intuitionistic analogues of Los's theorem, elementary embeddings, and countable saturation.
-
Intuitionistic Monotone Modal Logic: Proof Theory and Semantics
Introduces constructive neighbourhood semantics and an adapted structured calculus for intuitionistic monotone modal logic IM, proving decidability and noting analogies to classical variants of M and K.