Kripke completeness of strictly positive modal logics and related problems
Birkbeck, University of London
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.
Professor of Computer Science, Director of Research at Birkbeck, University of London. BSc and MSc (Moscow State University), PhD and Habilitation in Mathematics (Novosibirsk University). Research scientist at Keldysh Institute of Applied Mathematics (Russian Academy of Sciences), Alexander von Humboldt Foundation fellow (FU Berlin), Professor of Logic and Computation at King’s College London (2001-2005). Research interests: knowledge representation and reasoning (spatial, temporal, etc.), logic in computer science, in particular, modal and description logics.