Campus Event Calendar

Event Entry

What and Who

Labeled natural deduction for temporal logics

Marco Volpe
University of Verona
AG Audience

Date, Time and Location

Thursday, 16 December 2010
60 Minutes
E1 7


Despite the great relevance of temporal logics in many applications of computer science, their theoretical analysis is far from being concluded. In particular, we still lack a satisfactory proof theory for temporal logics and this is especially true in the case of branching-time logics.
In this talk, I will present a modular approach to the definition of labeled (natural) deduction systems for a large class of temporal logics. I will start with a system for the basic Priorean tense logics and show how to modularly enrich it in order to deal with richer and more complex logics, like LTL. I will also consider the extension to the branching case, focusing on the Ockhamist branching-time logics with a bundled semantics.
A detailed proof-theoretical analysis of the systems has been performed. In particular, in the case of discrete-time logics, for which rules modeling an induction principle are required, a procedure of normalization inspired to those of systems for Heyting Arithmetic has been defined.


Jennifer Müller
--email hidden
passcode not visible
logged in users only

Jennifer Müller, 12/07/2010 12:49 -- Created document.