Applications of deontic logic in areas such as intelligent legal information systems require the ability to represent at least two different notions of permission, one of which, ``free choice permission,'' cannot be adequately represented in standard modal logics. We define a logic which handles this modality by using ideas from dynamic logic. The logic is also able to expresses a different notion of permission corresponding to a lack of prohibition. The main result is the completeness of an axiomatization of the logic.
To appear in Journal of Logic and Computation --- A version of this paper appeared at the IEEE Symposium on Logic in Computer Science, Philadelphia, 1990.
postscript (72K)