Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = '5hh4tk2jh8o5h55von0k5gvq65' in /var/www/church/includes/database.mysql.inc on line 121
Jump from parallel to sequential proofs: Exponentials | Gruppo di Logica e Geometria della Cognizione

Jump from parallel to sequential proofs: Exponentials

Speaker:
Paolo Di Giamberardino
Quando:
07/05/2010 - 11:30
Dove:
Aula Verra, Facoltà di Lettere e Filosofia - Università Roma Tre, via Ostiense 234
Abstract

In previous works, by importing ideas from game semantics (notably Faggian-Maurel-Curien's ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called J-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using jumps (that is, untyped extra edges) as sequentiality constraints.

Starting from this result, in the present work we extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: more precisely, we replace the familiar linear logic notion of exponential box with a less restricting one (called cone defined by means of jumps. As consequence, we get a syntax for polarized nets where, instead of a structure of boxes nested one into the other, we have one of cones which can be partially overlapping. Moreover, we define normalization for exponential J-proof nets, proving, by Gandy's method, that even in case of ''superposed'' cones, reduction enjoys confluence and strong normalization.



Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = '5hh4tk2jh8o5h55von0k5gvq65' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/414', '', '216.73.216.58', 1751748763) in /var/www/church/includes/database.mysql.inc on line 121

Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: INSERT INTO sessions (sid, uid, cache, hostname, session, timestamp) VALUES ('5hh4tk2jh8o5h55von0k5gvq65', 0, 0, '216.73.216.58', '', 1751748763) in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/414', '', '216.73.216.58', 1751748763) in /var/www/church/includes/database.mysql.inc on line 121