A Hybrid Intuitionistic Logic: Semantics and Decidability

An intuitionistic, hybrid modal logic suitable for reasoning about distribution of resources was introduced in [14, 15]. The modalities of the logic allow us to validate properties in a particular place, in some place and in all places. We give a sound and complete Kripke semantics for the logic extended with disjunctive connectives. The extended logic can be seen as an instance of Hybrid IS5. We also give a sound and complete birelational semantics , and show that the semantics satisfies the finite model property: if a judgement is not valid in the logic, then there is a finite birelational countermodel. Hence we prove that the logic is decidable.

• Type: Journal
• Year: 2006
• Where: LOGCOM
• Authors: Rohit Chadha, Damiano Macedonio, Vladimiro Sassone
• Keywords: Complete Kripke Semantics, Hybrid Modal Logic, LOGCOM 2006, Logic