Campus Event Calendar
Event Entry
What and Who
Labeled natural deduction for temporal logics
Marco Volpe
University of Verona
Talk
RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 16 December 2010
11:00
60 Minutes
E1 7
2.01
Saarbrücken
Abstract
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.
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.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 12/07/2010 12:49 -- Created document.