TY - JOUR
AU - Fang, Liangda
AU - Wang, Kewen
AU - Wang, Zhe
AU - Wen, Ximing
PY - 2019/07/17
Y2 - 2021/04/14
TI - Disjunctive Normal Form for Multi-Agent Modal Logics Based on Logical Separability
JF - Proceedings of the AAAI Conference on Artificial Intelligence
JA - AAAI
VL - 33
IS - 01
SE - AAAI Technical Track: Knowledge Representation and Reasoning
DO - 10.1609/aaai.v33i01.33012817
UR - https://ojs.aaai.org/index.php/AAAI/article/view/4134
SP - 2817-2826
AB - <p>Modal logics are primary formalisms for multi-agent systems but major reasoning tasks in such logics are intractable, which impedes applications of multi-agent modal logics such as automatic planning. One technique of tackling the intractability is to identify a fragment called a normal form of multiagent logics such that it is expressive but tractable for reasoning tasks such as entailment checking, bounded conjunction transformation and forgetting. For instance, DNF of propositional logic is tractable for these reasoning tasks. In this paper, we first introduce a notion of logical separability and then define a novel disjunctive normal form SDNF for the multiagent logic K<sub>n</sub>, which overcomes some shortcomings of existing approaches. In particular, we show that every modal formula in K<sub>n</sub> can be equivalently casted as a formula in SDNF, major reasoning tasks tractable in propositional DNF are also tractable in SDNF, and moreover, formulas in SDNF enjoy the property of logical separability. To demonstrate the usefulness of our approach, we apply SDNF in multi-agent epistemic planning. Finally, we extend these results to three more complex multi-agent logics D<sub>n</sub>, K45<sub>n</sub> and KD45<sub>n</sub>.</p>
ER -