Natural Deduction for CTL - Proof Theory

Christian Renteria

CTL (Computation Tree Logic)[1] is a logic used both for the synthesis and for the verification of concurent programs. Usualy presented in the Hilbert style (axiomatic)[2], it has been adapted for sequent calculus[3], 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 labeled formulae 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 the induction rule.

[1] Clarke and Emerson, Design Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic - Lecture Notes in Computer Science 131.

[2] Goldblatt, Logics of Time and Computation - CSLI Lecture Notes 7.

[3] Echague, A Gentzen-System for Computation Tree Logic, In Proceedings of the XIX CLEI-PANEL Latin American Informatics Conference, Buenos Aires, 1993.

[4] Pravitz, Natural Deduction - Stockholm(1965)

[5] Proceedings of the Second Scandinavian Logic Symposium - Studies in Logic and the Foundation of Mathematics 63.

Address: Pontificia Universidade Catolica - Rio de Janeiro, Rua Joaquim Murtinho 675, Santa Teresa, Rio de Janeiro, CEP:20241, RJ, Brasil.

E-mail: chren@ibm.net, chren@inf.puc-rio.br