Natural Deduction Calculus for Computation Tree Logic

We 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.

• Type: Conference
• Year: 2006
• Where: JVA
• Authors: Alexander Bolotov, Oleg Grigoriev, Vasilyi Shangin
• Keywords: Applied Computing, JVA 2006, Natural Deduction, Temporal Logic, Temporal Logic Operators