Combining computation tree logic and deontic logic in natural deduction style calculus

In this technical report we present a natural deduction calculus for branching-time deontic logic, a combination of the branching-time logic CTL and deontic modalities and prove its correctness. The new proof technique can be applied as a reasoning tool in modeling dynamic normative systems, for example, social organisations. From the methodological point of view our approach allows to obtain similar proof systems for other modal extensions of CTL by simple modification of the part of the system that corresponds to the properties of modalities