RONCHI DELLA ROCCA	SIMONETTA
(cognome)	(nome)
Università degli Studi di TORINO	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
INF/01	Dipartimento di INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

ronchi@di.unito.it
(E-mail)

MASINI	ANDREA
(cognome)	(nome)

Professore ordinario	14/08/1958	MSNNDR58M14E625U
(qualifica)	(data di nascita)	(codice di identificazione personale)

Università degli Studi di VERONA	Facoltà di LETTERE e FILOSOFIA
(università)	(facoltà)
INF/01	Dipartimento di INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

045/8027922	045/8027928	masini@sci.univr.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

STUDI:
[1992] Dottore di Ricerca In Informatica, Pisa.
POSIZIONI:
[1993] Ricercatore Informatica, Facolta' SMFN, dip. Informatica, Univ. Pisa;
[Novembre 1998] Prof. Associato Informatica, Facolta' SMFN, dip. Matematica, Univ. Trento.
[Ottobre 2001] Prof. Straordinario, Facolta' Lettere e Filosofia, dip. Informatica, Univ. Verona.
VISITATORE:
[Gennaio 1990--Luglio 1990], L.I.T.P. del CNRS, Universite` Paris VII, Parigi.
RELAZIONI INVITATE:
-International Workshop on Proof Theory of Modal Logic. Hamburg, Germania, November 19-20, 1993.
-First international conference on Natural Deduction. Rio de Janeiro, Luglio 2001.
SUPERVISIONE DOTTORANDI:
Fabio Martinelli: tesi di dottorato su logiche per problemi di sicurezza;
Davide Marchignoli: tesi di dottorato su teoria della dimostrazione per logiche temporali.
INTERESSI DI RICERCA:
-logica lineare;
-teoria dei tipi;
-teoria della dimostrazione;
-logiche modali e temporali.

Testo inglese

STUDIES:
[1992] PhD in Computer Science, Pisa.
POSITIONS:
[1993] Assistant Professor of Comp.Sci., Univ. Pisa;
[November 1998] Associate Professor of Comp.Sci., Univ. Trento.
[October 2001] Full Professor of Comp.Sci., Univ. Verona.
VISITING:
[Jan. 1990-July 1990] L.I.T.P. of french CNRS,
Universite` Paris VII, Paris.
INVITED TALKS:
-International Workshop on Proof Theory of Modal Logic. Hamburg, Germania, November 19-20, 1993.
-First international conference on Natural Deduction. Rio de Janeiro, July 2001.
PhD-Students SUPERVISION:
Fabio Martinelli: phd thesis on logics for security problems;
Davide Marchignoli: phd thesis on proof theory for temporal logic.
RESEARCH INTERESTS:
-linear logic;
-type theory;
-proof theory;
-modal and temporal logics.

1. GUERRINI S., MARTINI S., MASINI A. (?). Coherence for sharing proof-nets. THEORETICAL COMPUTER SCIENCE. ISSN: 0304-3975 IN STAMPA.
2. GUERRINI S., MARTINI S., MASINI A. (2001). Proof nets, garbage, and computations. THEORETICAL COMPUTER SCIENCE. vol. 253, pp. 185-237 ISSN: 0304-3975 .
3. GUERRINI S., MASINI A. (2001). Parsing MELL proof nets. THEORETICAL COMPUTER SCIENCE. vol. 254/1-2, pp. 317-335 ISSN: 0304-3975 .
4. GUERRINI S., MARTINI S., MASINI A. (1998). An analysis of (linear) exponentials based on extended sequents. LOGIC JOURNAL OF THE IGPL. vol. 6, pp. 735-753.
5. MARTINI S., MASINI A. (1997). Experiments in Linear Natural Deduction. THEORETICAL COMPUTER SCIENCE. vol. 176, pp. 159-173 ISSN: 0304-3975 .

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						2002	2003
Personale docente:
1	MASINI	ANDREA	INFORMATICA	Prof. ordinario	INF/01	8 (ore: 1100)	10 (ore: 1375)
2	BELLIN	GIANLUIGI	INFORMATICA	Ricercatore	MAT/01	6 (ore: 825)	6 (ore: 825)
3	SOLITRO	UGO	INFORMATICA	Ricercatore	INF/01	3 (ore: 411)	10 (ore: 1375)
Altro personale:

1.7.2 Personale universitario di altre Università

Nº	Cognome	Nome	Università	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							2002	2003
Personale docente:
Altro personale:

1.7.3 Titolari di assegni di ricerca

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo
					2002	2003
1	FLEURY	ARNAUD	Dip. SCIENTIFICO E TECNOLOGICO	2002	11 (ore: 1507)	0

1.7.4 Titolari di borse per Dottorati di Ricerca e ex L. 398/89 art.4 (post-dottorato e specializzazione)

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo

1.7.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	assegnista di ricerca	14300	11  (ore: 1507)

1.7.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Ente	Qualifica	Mesi uomo

Testo italiano

Logica Lineare: verso una logica delle prove

Testo inglese

Linear Logic: towards a logic of proofs

Testo italiano
LOGICA LINEARE ; TEORIA DELLA DIMOSTRAZIONE ; LOGICA INTUIZIONISTA ; LOGICA CLASSICA ; INTERAZIONE ; COMPLESSITA' COMPUTAZIONALE ; TEORIA DELLE CATEGORIE ; COMPUTAZIONI DISTRIBUITE ; PRAGMATICA

Testo inglese
LINEAR LOGIC ; PROOF THEORY ; INUITIONISTIC LOGIC ; CLASSICAL LOGIC ; INTERACTION ; COMPUTATIONAL COMPLEXITY ; CATEGORY THEORY ; DISTRIBUTED COMPUTATIONS ; PRAGMATIC

Testo italiano

La logica Lineare (LL) [GIR87] ha fornito una nuova motivazione allo sviluppo della teoria della dimostrazione o piu' propriamente (seguendo G.Kreisel) alla teoria delle prove. L'idea fondante della Logica Lineare e' quella di una logica costruttiva che consente di rivelare le informazioni usualmente nascoste nei sistemi formali usuali [GIR91]. Tale aspetto e' ben illustrato dalla decomposizione dell'implicazione intiuzionista A->B in !A -o B, ovvero in una implicazione lineare "-o" piu' un operatore (l'esponenziale "!"[MM95]) responsabile della duplicazione e cancellazione logica (contrazione e indebolimento). Uno degli aspetti piu' caratteristici della Logica Lineare riguarda la rappresentazione delle dimostrazioni tramite reti di prova (proof-nets)[GIR87]. Prima dell'arrivo in scena della logica lineare c'erano essenzialmente due possibili formulazioni per le dimostrazioni, la deduzione naturale ed il calcolo dei sequenti. In entrambi i sistemi deduttivi le dimostrazioni sono generate induttivamente. Era una convinzione generale che ogni ragionevole calcolo logico dovesse avere una struttura induttiva basata sull'applicazione di regole preservanti la correttezza. Girard ha cambiato questo punto di vista tramite le reti di prova. Le reti di prova non sono definite induttivamente, esse sono (iper)grafi liberamente generati tramite regole logiche locali e verificanti un opportuno criterio geometrico di correttezza [GM01, GUE99]. In analogia con il caso della logica intuizionista, potremmo dire che le reti di prova sono una forma di lambda calcolo associato alla Logica Lineare. Il processo di semplificazione delle reti di prova (che corrisponde all'eliminazione dei tagli) e' ora uno strumento importante nell'analisi dei processi computazionali dei sistemi logici, ma pure in un senso piu' generale. Ad esempio al fine di effettuare il processo di eliminazione dei cut e' stato definito il concetto di riduzione locale ed asincrona (con costo unitario)[GMM01]; tale idea e' stata centrale nell'analisi delle riduzioni ottimali [Lam90,Lev78] dei linguaggi funzionali (e piu' generalmente nei sistemi di interazione) [GMM02,LAF95,GAL92,AM98]. Il concetto di logica come metodo per il controllo della complessita' ha dato origine allo studio di particolari logiche lineari con buoni aspetti computazionali. Di particolare rilevanza e' lo studio della classe P delle funzioni calcolabili in tempo polinomiale: in [GIR98] Girard ha proposto una logica per il tempo polinomiale, cioe' un sistema logico intrinsecamente in tempo polinomiale, non semplicemente un'assiomatizzazione di P. L'idea cruciale e' la definizione di una logica lineare (detta Logica Lineare Leggera o LLL) nella quale e' rappresentabile (ossia corrisponde ad una dimostrazione di LLL) ogni funzione in P e viceversa ogni dimostrazione in LLL e' riducibile in tempo polinomiale. Questo metodo e' completamente nuovo e ha prodotto un approccio differente allo studio della complessita' computazionali, suggerendo di conseguenza alcune nuove tecniche per confrontare classi computazionali.
Negli anni 90 molti autori hanno rivisitato il problema della normalizzazione forte e della confluenza per la logica classica nelle formalizzazione del calcolo dei sequenti LK o in deduzione naturale. La vasta letteratura che si ricollega a [DJS97,GIR91,PAR97] condivide il presupposto che il fallimento di queste proprieta` in LK e` dovuta ad una mancanza di informazione (piu` precisamente, di focalizzazione) che si puo` fornire direttamente oppure attraverso traduzioni in logica intuizionistica o lineare. Recentemente [UB00] la ricerca si e` rivolta alla caratterizzazione della logica classica attraverso assegnazioni di termini al calcolo dei sequenti; le reti di prova per la logica affine [BELa] o classica sono una diretta generalizzazione delle reti di prova per la logica lineare nella formulazione di [BW95] e forniscono un formalismo piu` semplice della assegnazione di termini.
Oltre ai campi usuali di applicazione della LL ci sono nuove e promettenti aree di ricerca. Una di queste e' data dallo studio della "pragmatica" (vedere per esempio la teoria assiomatica delle fondazioni delle leggi sviluppata da L.Ferrajoli in [FE99]). Tra i differenti approcci alla pragmatica particolarmente interessante e' quello di Dalla Pozza e Garola [DPG95,DP97] ulteriormente sviluppato in [BDP01] dove agli operatori che esprimono asserzioni, congetture, obbligazioni e permessi, e' stata aggiunta l'implicazione lineare vista come implicazione causale

Testo inglese

Linear Logic (LL) [GIR87] has given a new motivation to the development of proof theory or more properly (following G.Kreisel) to the theory of proofs. The founding idea underlying Linear Logic is that of a constructive logic that reveals the information usually hidden in the standard formal systems [GIR91]. Such a feature is well illustrated by the decomposition of the intuitionistic implication A->B into !A -o B, namely in a linear implication "-o" plus an operator (the exponential ! [MM95]) which is responsible of the logical duplication and erasing (contraction and weakening). One of the most distinctive aspects of Linear Logic is about the representation of proofs by means of proof-nets [GIR87]. Before the arrival on the scene of linear logic there were essentially two possible formulations for proofs, natural deduction and sequent calculus. In both the deductive systems proofs are inductively generated. It was generally believed that any reasonable logical calculus should have such a kind of inductive structure based on the application of preserving correctness rules . Girard changed this point of view by means of proof-nets. Proof-nets are not inductively defined, they are (hyper)graph freely generated by means of local logical rules and verifying a suitable global geometrical correctness criterion [GM01, GUE99]. In similarity with intuitionist logic, we could say that proof-nets are a kind of lambda calculus associated to Linear Logic . The process of simplification of proof-nets (corresponding to cut elimination) is now an important tool in the analysis of computational processes inside logical systems, but also in a more general perspective. For instance in order to perform cut elimination has been defined the concept of local and asynchronous (with unitary cost)[GMM01] proof-net reduction; this idea has been central in the analysis of optimal reductions [Lam90,Lev78] in functional languages (and more generally in interaction systems) [GMM02,LAF95,GAL92,AM98]. In addition the concept of logic as a method for the control of complexity has originated the study of special linear logics with nice computational features. Of particular relevance is the study of the class P of poly-time functions: in [GIR98] Girard has proposed a logic for poly-time that is a logical system "intrinsically poly-time" (not simply an axiomatization of poly-time). The crucial idea is the definition of a linear logic (called Light Linear Logic or LLL) in which any poly-time function is representable (namely, it correspond to a LLL proof) and vice versa every proof in LLL is poly-time reducible. This approach is absolutely new and has produced a different approach in the study of computational complexity, hence suggesting some new methods for comparing computational classes.
In the 1990s many authors have revisited the problem of strong normalization and confluence for classical logic as formalized in LK or in systems of natural deduction. The large amount of literature related to [DJS97,GIR91,PAR97] shares the presupposition that the failure of both strong normalization and confluence in LK is due to a lack of information (more precisely, of focalization) which can be supplied either explicitly or through translations into intuitionistic or linear logic. Recently [UB00] the search has been directed towards an independent characterization of classical logic through term-assignments to the sequent calculus; proof-nets for affine [BELa] and classical logic are a straightforward generalization of proof-nets for linear logic as formulated in [BW95] and provide a simpler formalism than term-assignments.
In addition to usual fields of application of LL there are new promising research areas. One of these is given by the study of "pragmatic" (see for example the axiomatic theory of the foundations of laws developed by L.Ferrajoli in [FE99]). Among different approaches to pragmatics particularly interesting is those of Dalla Pozza and Garola [DPG95,DP97] further developed in [BDP01] where to the operators which express assertions, conjectures, obligations and permissions has been added the linear implication regarded as causal implication.

[AM98] ASPERTI A., MAIRSON H. (1998). Parallel beta reduction is not elementary recursive. Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 303-315.
[BDP01] BELLIN G., DALLA POZZA C. (2001). A pragmatic interpretation of substructural logics in Reflection on the Foundations of Mathematics: Essays in honor of Solomon Feferman. W. Sieg. R. Sommer and C. Talcott eds. Lecture Notes in Logic. Association for Symbolic Logic. vol. 15.
[BELa] BELLIN G. (to appear). Two paradigms of logical computation in Affine Logic?. in Logic for Concurrency and Synchronization. R. de Queiroz (ed.). Trends in Logic. Kluwer.
[BErio] BELLIN G. Towards a formal pragmatics, submitted to "Natural Deduction, Rio 2001" (Festschrift for Dag Prawitz).
[BW95] BELLIN G., VAN DE WIELE J. (1995). Subnets of Proof-nets in MLL-. in Advances in Linear Logic, J.-Y. Girard, Y. Lafont. L. Regnier (Eds.). number 222 of the London Mathematical Society Lecture Note Series. Cambridge University Press. pp.249-270.
[Bar91] BARR M. (1991). *-autonomous categories and linear logic. Mathematical Structures in Computer Science 1, pp. 159-178.
[CAR97] CARBONE A. (1997). Turning cycles into spirals. Annals of Pure and Applied Logic. 96:57-73.
[CAR97a] CARBONE A. (1997). Duplication of directed graphs and exponential blow up of proofs. Annals of Pure and Applied Logic. 100:1-76.
[DJS97] DANOS. V., JOINET J-B., SCHELLINX. H. A. J. M. (1997). A new deconstructive logic: classical logic. Journal of Symbolic Logic. 62(3). pp. 755-807.
[DP97] DALLA POZZA C. (1997). Una logica prammatica per la concenzione ``espressiva'' delle norme. In A. Martino. ed. Logica delle Norme. Pisa.
[DPG95] DALLA POZZA C., GAROLA C. (1995). A pragmatic interpretation of intuitionistic propositional logic. Erkenntnis. Vol 43. pp. 81-109.
[FE99]FERRAJOLI L. (1999) ASPETTATIVE E GARANZIE. Prime tesi di una teoria assiomatizzata del diritto. In AA. VV. Logos dell'Essere - Logos della Norma. Studi per una ricerca coordinata da Luigi Lombardi Vallauri. Adriatica Editrice. Bari.
[FM98] FERNANDEZ M., MACKIE I. (1998). Interaction Nets and Term Rewriting Systems. Theoretical Computer Science. 190(1):3-39.
[Fle96] FLEURY A. (1996). La règle d'échange: Logique linéaire multiplicative tressée PhD Thesis, Université Denis Diderot, Paris VII.
[GAL92] GONTHIER G., ABADI M., LEVY J-J (1992). Linear logic without boxes. 7th LICS. pp. 223-234. IEEE Press.
[GIR87] GIRARD J.-Y. (1987). Linear Logic. theoretical computer science. 50(1). pp. 1-102.
[GIR91] GIRARD. J-Y. (1991). A new constructive logic: classical logic. Mathematical Structures in Computer Science. 1(3): 255-296.
[GIR98] GIRARD., J-Y. (1998). Light linear logic. Information and Computation. 143 no. 2. pp. 175--204.
[GM01] GUERRINI S., MASINI A. (2001). Parsing MELL proof nets. theoretical computer science. vol. 254/1-2, pp. 317-335 ISSN:0304-3975 .
[GMM01] GUERRINI S., MARTINI S., MASINI A. (2001). Proof nets, garbage, and computations. theoretical computer science. vol. 253, pp. 185-237.
[GMM02] GUERRINI S., MARTINI S., MASINI A. (?). Coherence for sharing proof-nets. theoretical computer science. IN STAMPA.
[GMM98] GUERRINI S., MARTINI S., MASINI A. (1998). An analysis of (linear) exponentials based on extended sequents. logic journal of the igpl. vol. 6, pp. 735-753.
[GUE99] GUERRINI S. (1999). Correctness of multiplicative proof nets is linear. In Proceedings of 14th Annual Symposium on Logic in Computer Science (LICS '99). Trento. Italy. IEEE pp.454-463
[LAF95] LAFONT Y. (1995). From Proof-Nets to Interaction Nets. in Advances in Linear Logic, J.-Y. Girard, Y. Lafont. L. Regnier (Eds.). number 222 of the London Mathematical Society Lecture Note Series. Cambridge University Press. pp. 225-247.
[Lam90] LAMPING J. (1990). An algorithm for optimal lambda-calculus reduction. 17th ACM POPL. pp. 16-30. ACM Press.
[Lev78] LEVY J.-J. (1978). Reductions correctes et optimales dans le lambda-calcul. PhD thesis. Univ. Paris VII.
[MM95] MARTINI S., MASINI A. (1995). On the fine structure of the exponential rule, in Advances in Linear Logic, J.-Y. Girard, Y. Lafont. L. Regnier (Eds.). number 222 of the London Mathematical Society Lecture Note Series. Cambridge University Press. pp. 197--210.
[MM97] MARTINI S., MASINI A. (1997). Experiments in Linear Natural Deduction. theoretical computer science. vol. 176, pp. 159-173.
[PAR97] PARIGOT M. (1997). Proofs of Strong Normalization for Second Order Classical Natural Deduction. The Journal of Symbolic Logic. (62)4. pp. 1461-1479.
[UB00] URBAN. C., BIERMAN. G. M. (2000). Strong Normalization of Cut-Elimination in Classical Logic. Fundamenta Informaticae XX. pp. 1-32.

Testo italiano

L'attivita' dell'unita' di Verona seguira' cinque linee di ricerca:
1) logiche per classi di complessita' computazionale;
2) teoria strutturale della dimostrazione;
3) semantica categoriale della logica lineare;
4) generalizzazioni delle reti di prova;
5) pragmatica formale.
In (1) ci proponiamo di studiare tramite logiche lineari classi di complessita' computazionali seguendo la linea di ricerca indicata da Girard con la logica lineare "leggera" (Light LL). In particolare intendiamo studiare la possibilita' di introdurre nuovi connettivi per rappresentare costrutti non deterministici. L'obiettivo e' quello di arrivare ad una buona formulazione logica di classi di complessita' nondeterministiche (in prima istanza NP). Le logiche lineari "non deterministiche" saranno inoltre studiate tramite adeguate estensioni delle reti di prova seguendo il paradigma delle computazioni locali ed asincrone. Al fine di trattare computazioni locali asincrone sara' necessario avere una gestione locale della dinamica del non determinismo, gestione che ci proponiamo di ottenere tramite nuovi nodi di controllo. Ci aspettiamo che i nuovi nodi di controllo per il nondeterministico abbiano qualche similarita' con i ben conosciuti nodi di controllo usati nel caso delle riduzioni delle reti condivise (i cosiddetti fan).
In (2) si studieranno le proprieta` caratteristiche della normalizzazione delle prove in logica classica, identificate nel non-determinismo e nel trattamento dell'irrilevanza e della focalizzazione. Le prove classiche saranno rappresentate per mezzo delle reti di prova, secondo la definizione standard con regole strutturali esplicite ma anche secondo formulazioni alternative, anche allo scopo di contribuire alla difficile questione dell'identita` delle prove classiche.
In (3) intendiamo studiare la semantica categoriale della logica lineare moltiplicativa nel contesto piu' generale possibile. Per esempio la regola di scambio dovrebbe essere considerata "intrecciata" (braided); daremo un teorema di coerenza per le categorie "ribbon braided *-autonomous". La relazione tra la formulazione intuizionista e quella classica dovra' essere chiarita in un contesto non commutativo e intrecciato. In particolare in tale contesto studieremo le costruzioni di Chu; studieremo inoltre le versioni intuizioniste complete di tali sistemi. Il terzo aspetto importante sara' quello di generalizzare le costruzioni proposte al caso del par pre monoidale.
In (4) partendo dalle proof-nets di Girard e dai logical flow graphs (Buss, Carbone) ci si propone di studiare il ruolo di stutture generali per la rappresentazione di dimostrazioni (principalmente, ma non solo, nell'ambito della logica lineare). Lo scopo e' di ottenere un'analisi piu' fine degli aspetti funzionali (e non funzionali) della normalizzazione dei sistemi deduttivi, in particolare quelli "lineari".
In (5) ci si propone di sviluppare un sistemi logico (LP) per la pragmatica basato su una semantica classica multi modale ed una pragmatica intuizionistica, che utilizza l'implicazione lineare per rappresentare la causalita` e l'interazione di processi. La proiezione della pragmatica sul livello semantico si basa su una estensione della interpretazione di Goedel, McKinsey e Tarski della logica intuizionistica in S4, in cui gli operatori espressivi di asserzioni e congetture corrispondono aglil operatori di interno e di chiusura (oppure di necessita` e possibilita`) nell'interpretazione topologica (o modale) della logica intuizionistica e nell'interpretazione duale. L'azione della semantica classica sulla pragmatica permette invece un nuovo approccio alla formalizzazione di frammenti costruttivi della logica classica. Il sistema proposizionale esistente verra` esteso al primo ordine; si considerera` anche l'introduzione di operatori modali indiciati tipici delle logiche della conoscenza. Il sistema (LP) potrebbe in futuro avere applicazioni anche alla assiomatizzazione dei fondamenti del diritto e alla formalizzazione dell'argomentare giuridico.

Testo inglese

The activity of the Verona unit will follow five lines of research:
1) logics for computational complexity classes;
2) structural proof theory;
3) categorical semantics of linear logic;
4) generalizations of proof nets;
5) formal pragmatics.
In (1) we intend to study, by means of linear logics, computational complexity classes following the research line begun by Girard with Light Linear Logic. In particular we are interested in the introduction of new connectives in order to deal with non deterministic constructions. Our attempt will be to obtain a good logical formulation of nondeterministic complexity classes (in particular the class NP). We plan to investigate the "non deterministic" linear logics by means of suitable extensions of proof nets following the local and asynchronous paradigm. In order to deal with local and asynchronous computations, a local management of the dynamic of non determinism will be necessary, we expect to obtain such a management by means of suitable new control nodes. We guess that the new control nodes for nondeterminism will have some similarity with the behavior of the well known control nodes used in the case of reduction of shared nets (the so called fans).
In (2) we shall study the properties of normalization of proofs (cut-elimination) in classical logic. Non-determinism, the treatment of irrelevance and of focalization appear as distinguishing features of classical normalization, by contrast with those of intuitionistic and linear logic. Classical proofs shall be represented through proof-nets, according to the standard definition with explicit structural rules, but also considering alternative formulations, with the aim of contributing to the difficult issue of the identity of proofs in classical logic.
In (3) we intend to study the categorical semantics of multiplicative linear logic in the most possible general setting. For example, the exchange rule should be considered as braided; thus we will give a coherence theorem for ribbon braided *-autonomous categories. The relationship between the intuitionistic and the classical setting has to be clarified in the non-commutative, mixed and braided systems. In particular we will study the Chu constructs in these setting; we will also study De Paiva's full intuitionistic variants of those systems. The third important aspect will be to generalize those structures when the par is only pre-monoidal.
In (4) starting from the proof-nets (Girard) and the logical flow graphs (Buss, Carbone) we want to study more general structures for the representation of logical proofs, mainly - but not exclusively - in a linear framework. We intend to provide tools for an effective analysis of the normalization process in a really abstract milieu.
In (5) we intend to develop a logical system (LP) for formal pragmatics, based upon a multi-modal classical semantics and an intuitionistic pragmatics, which uses linear implication to represent causality and process interaction. The projection of pragmatics onto semantics is based on an extension of Goedel's and McKinsey and Tarski's interpretation of intuitionistic logic in S4, where operators expressing assertions and conjectures correspond to interior and closure operators (or necessity and possibility operators) in the topological (or modal) interpretation of intuitionistic logic and in the dual interpretation. The action of classical semantics on pragmatics yields a new approach to the formalization of constructive fragments of classical logic. The existing propositional system will be extended to first order. An extension through indexed modal operators proposed in some epistemic logics will also be considered. In the future the system (LP) could be applied also to the axiomatization of the foundations of laws and to the formalization of legal reasoning.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese

Attrezzatura I
Descrizione

valore presunto ( Euro)   percentuale di utilizzo per il programma

Attrezzatura II
Descrizione

valore presunto ( Euro)   percentuale di utilizzo per il programma

QUADRO RD

4.1.1 Altro

QUADRO RA

4.2.1 Altro

Firma ____________________________________________

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati; legge del 31.12.96 n° 675 sulla "Tutela dei dati personali")