Modal logics, Horn theories, and (hyper-)graph theory are not so far - The 'enumeration problems' bridge

In this talk, we will explore a connection between the fields of modal logics, Horn theories, and hyper-graph theory. The gap is bridged by the enumeration problem MaxMod, that is, the problem of enumerating the maximal models of a given Horn theory. On the one hand, we will show that MaxMod is polynomially reducible to the problem of enumerating the subsets of modalities (featured by a given modal logic) which do not define a distinguished modality. Such a problem is crucial to address expressiveness issues for modal logics. On the other hand, we will show that the restriction of MaxMod to a particular class of instances amounts to the well-studied problem of enumerating minimal hitting sets of hyper-graphs, whose exact complexity characterization wrt the complexity hierarchy for enumeration problems is still unknown. We will also present an algorithm for MaxMod and we give experimental evidence about its effectiveness.