Topic Archive: Kripke models
We consider the fragment of propositional multi-modal logic that consists of implications whose premise and conclusion are strictly positive (SP) modal formulas constructed from propositional variables using conjunction and unary diamond operators. SP-logics can be interpreted over bounded meet-semilattices with normal monotone operators (SLOs, for short), and over first-order structures (aka Kripke frames). The former interpretation provides natural calculi for SP-logics, while reasoning over the latter can be supported by modern provers and description logic reasoners, and is often tractable. An SP-logic is called (Kripke) complete if it has the same consequences in each of these semantics. This talk reports on our first steps in developing completeness theory for SP-logics, which turns out to be quite different from classical completeness theory for modal logics. We also consider some related problems, in particular, axiomatisability and computational complexity.