A natural deduction system for ctl
Christian Jacques Renterıa, Edward Hermann Hæusler · 2002
CTL (Computation Tree Logic) [3] is a logic used both for the synthesis and for the verification of concurrent programs. Usually presented in the Hilbert style (axiomatic) [6], it has been adapted for sequent calculus [4], but without normalization. The aim of the present work is to present a Natural Deduction system for CTL. For that reason the original language has been modified, and labelled formulas have been used. It has been proved that the system is correct and complete. Then the possibility of normalizing the proofs is studied and it is seen, as expected, that strong normalization is achieved in the system without