A Hybrid Intuitionistic Logic: Semantics and Decidability
Rohit Chadha, Damiano Macedonio, Vladimiro Sassone · Journal of Logic and Computation · 2006
We study a hybrid intuitionistic modal logic suitable for reasoning about distribution of resources. The modalities of the logic allow validation of properties in a particular place, in some place and in all places. We provide a sound and complete Kripke semantics. We also define a sound and complete birelational semantics, and show that it enjoys the finite model property: if a judgement is not valid in the logic, then there is a finite birelational counter-model. Hence, we prove that the logic is decidable.