A dynamic deontic logic for complex contracts (Q444496)

This paper presents a dynamic deontic logic for contracts, not only software contracts, web services, etc., but especially legal contracts. This affects the design of the system. Distinctive here is its stance of the ought-to-do, whereby deontic modalities apply to complex actions, rather than propositions as in so much of deontic logic. In addition, each modality is indexed by a clause indicating a reparation in case of violation. Further, the deontic modalities are added to a dynamic logic in order to allow reasoning about sequences of actions, and also synchronous actions. Unlike other dynamic logics, this considers deterministic actions. In addition to the formal analysis and representation of the applicable concepts, the principal result here is to establish that the deontic modalities over synchronous actions have the tree model property, and hence are decidable. Further, many familiar properties of the deontic modalities are indicated, as well as how the present system avoids many of the standard paradoxes of deontic logic.