Modeling Deontic Modal Logic in ASP

We consider the problem of implementing deontic modal logic.We show how (deontic) modal operators can be elegantly and directly expressed using default negation (negation-as-failure) and strong negation present in answer set programming (ASP).We propose using global constraints of ASP to represent obligations, prohibitions, and permissions in deontic modal logic.We show that our proposed representation results in the various decades-old paradoxes of deontic modal logic being simply and elegantly resolved.Our method also serves as a means for modeling conditional obligations and conditional prohibitions in knowledge representation.The fact that ASP asserts the denial :-p, -p. for every proposition p ensures that axiom D holds for the ASP modeling of alethic modal logic.D: □p → ¬□¬p = trueWith this observation, the modal square of opposition automatically follows (see Fig. 2 in [25]), i,e, the modal square of opposition states that if p is necessary, it is possible, and if p is impossible, then it is not necessary.In ASP, if p is true, then -p must be false, which implies that not -p (possible p) holds; and if p is impossible, then -p is true, so p must be false, and so not p (p is not necessary) is true.As stated earlier, strong negation captures the notion of impossibility, while negation-as-failure captures the notion of the modal not operator.The □ (necessity) operator disappears due to the alethic modal logic rule: □p → p.With the mapping described above, formulas of alethic modal logic can be encoded in ASP and their satisfiability checked.