A Tableaux System for Deontic Action Logic

In [1] and [2] we have introduced a novel deontic action logic for reasoning about fault-tolerance. In this paper we present a tableaux method for this logic; this proof system is sound and complete, and because the logic has the usual boolean operators on actions, it also allows us to deal successfully with action complement and parallel execution of actions. Finally, we describe an example of application of this proof system which shows how the tableaux system can be used to obtain (counter-) models of specifications.