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

Adaptive Agents and Multi-Agents Systems, pp. 740–748

Abstract

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 K(D)45_n and S5_n. 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.

Authors 4

1. Qihui Feng Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Hannah M. Wilk Aachen

   University of Amsterdam · RWTH Aachen University

   Affiliation as printed

   University of Amsterdam & RWTH Aachen University, Amsterdam, Netherlands

3. Shakil M. Khan

   University of Regina

   Affiliation as printed

   University of Regina, Regina, SK, Canada

4. Gerhard Lakemeyer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany