Natural Deduction Calculus for Computation Tree Logic

Abstract

The authors present a natural deduction calculus for the computation tree logic, CTL, defined with the full set of classical and temporal logic operators. The system extends the natural deduction construction of the linear-time temporal logic. This opens the prospect to apply our technique as an automatic reasoning tool in a deliberative decision making framework across various applications in AI and computer science, where the branching-time setting is required