Description
Meet-semilattices with monotone operators (SLOs) are reducts of Boolean algebras with normal and additive operators (BAOs). (BAOs are well-known algebraisations of propositional multimodal logic ML. SLOs correspond to a `positive implicational' fragment of ML, which has been studied in knowledge representation&reasoning and also in provability logics.)
We discuss three kinds of problems in connection with SLOs:
1) BAO-to-SLO conservativity. Given a SLO-type equational theory E and a SLO-type equation e, one can consider two consequence relations for `E implies e':one over BAOs, and a second one over SLOs. We show that in general the problem whether for a finite E BAO-consequence is conservative over SLO-consequence is undecidable. Still, we started a systematic study of the conservativity problem for different E's, depending on the form of their first-order correspondent (in the modal logic sense), and developed two general methods for proving conservativity.
2) Decision problems. We have several results contrasting the computational complexity of SLO-consequence with that of BAO-consequence.
3) Definability of relational constraints by SLO-type equations. We developed some semantical tools for testing definability, and obtained many examples of definable and non-definable (but modally definable) relational properties.
Joint work with S.Kikot, Y.Tanaka, M.Zakharyaschev and F.Wolter