A Complete and Compact Deontic Logic

PABLO F. CASTRO; T.S.E. MAIBAUM

LECTURE NOTES IN COMPUTER SCIENCE

Springer Verlag

Lugar: Springer Berlin; Año: 2007 vol. 4711 p. 109 - 123

0302-9743

In this paper we present a propositional deontic logic, with  the goal of using it to specify fault-tolerant systems, and an axiomatization of it. We prove several results about this logic: completeness, soundness, compactness and decidability. The main technique used during the completeness  proof is based on standard techniques for modal logics, but it has some new characteristics introduced for dealing with this logic. In addition, the logic provides several operators which appear useful for use in practice, in particular to model fault-tolerant systems and to reason about their fault tolerance properties.