Translating Multi-Agent Modal Logics of Knowledge and Belief into Decidable First-Order Fragments

Translation-based modal theorem proving has been studied for decades. By reducing modal formulae to fragments of first-order logic, methods developed for first-order reasoning can be applied to modal inference problems. However, the existing translation approaches are insufficient for modal systems with specific frame properties, such as transitivity or Euclideanity, since they result in formulae not in a decidable first-order fragment. With a revisit of the set-based possible-worlds semantics, we propose a new translation for multi-agent modal systems of knowledge and belief, such as 𝐾 (𝐷)45 𝑛 and 𝑆5 𝑛. We prove that the resulting formulae of the translation are in the two-variable guarded fragment. Therefore the decidability of the general satisfiability problem is preserved and it paves the way for translation-based reasoning in these modal systems. We also extend our approach to first-order modal logic and consider a decidable fragment.