Reasoning about permissions and obligations sometimes requires to distinguish more than one level of permission: certain actions are preferable to others, or one has more confidence in one type of action achieving the same goal than in other. We give a logic handling this type of ramification, and present a complete axiomatization. The recent work offers an extension of the Dynamic Logic of Permission defined by Meyden [The dynamic logic of pernission, Journal of Logic and Computation, 1996, pp. 465-479], where a two-level system was presented. We also prove a separation theorem for the multi-level permission formulas.
Keywords. Dynamic logic; deontic logic; Kripke-model; axiomatization; logic of permission
Full paper(PDF, 150k)