Two-sorted Modal Logic for Formal and Rough Concepts

In this paper, we propose two-sorted modal logics for the representation and reasoning of concepts arising from rough set theory (RST) and formal concept analysis (FCA). These logics are interpreted in two-sorted bidirectional frames, which are essentially formal contexts with converse relations. On one hand, the logic $\mathbf{\text{KB}}$ contains ordinary necessity and possibility modalities and can represent rough set-based concepts. On the other hand, the logic $\mathbf{\text{KF}}$ has window modality that can represent formal concepts. We study the relationship between $\mathbf{\text{KB}}$ and $\mathbf{\text{KF}}$ by proving a correspondence theorem. It is then shown that, using the formulae with modal operators in $\mathbf{\text{KB}}$ and $\mathbf{\text{KF}}$, we can capture formal concepts based on RST and FCA and their lattice structures.