3 Jun 1992 15:17

### Interpreting 1st order logic in linear logic

Date: Tue, 2 Jun 92 14:36:58 +0200

Some days ago I posted a question about Linear Logic. I got several replies
of people interested to the question, but only two answers. I mail
them for sake of completness.

S. Berardi

Date: Mon, 25 May 92 15:55:54 +0200

A quick question to linear people:
what is the simplest interpretation of First Order Classical Logic in Linear
Logic known up to now?
Of course I heard of several of them, but I found all of them a bit tricky.
I consider only complete interpretations, i.e. mapping:

Phi: {First Order Classical Formulas} -> {First Order Linear Formulas}

such that A is a classical theorem iff Phi(A) is a linear theorem.
Please answer me, not to the net, since I suppose the argument be widely
known, except by me!

S. Berardi

>From murthy@... Wed May 27 14:52:24 1992

Hi, Stefano,

Every interpretation of CL into CLL that I know of factors THRU a
translation of CL into IL.  Thus, if one wants to know what equations


4 Jun 1992 19:18

### Coq Release Info

Date: Thu, 4 Jun 92 18:54:58 +0200
To: distribution: <at> inria.fr; (see end of body)

First of all, all my apologies if you receive multiple versions of this
message because you are in the intersection of several mailing lists.

This is an announcement for the release of an improved version of Coq,
our Proof Assistant for the Calculus of Inductive Constructions.

Coq is freely available by ftp as follows:
ftp nuri.inria.fr
or ftp 128.93.1.26
Then do
binary
cd INRIA/coq
get coq.tar.Z
quit

Coq runs in CAML V3.1, also available on the same machine in directory
INRIA/caml/V3.1. Versions are currently available for the following machines:
Sun3, Sun4, Decstation, SONY68k, SONYR3000, Apollo, and Macintosh/AUX.
Coq has also an experimental version on top of caml-light, a smaller and more
portable implementation of ML.

We shall appreciate all comments, suggestions, bug reports.
Send such mail to: coq@...


4 Jun 1992 20:38

### Games and sequentiality

Date: Wed, 03 Jun 92 09:57:31 -0700

The following set of preliminary results, which I would like to bring to
the attention of types readers, seems to indicate that there is a nice
relation between games and sequentiality.

CONCRETE DATA STRUCTURES, SEQUENTIAL ALGORITHMS, AND LINEAR LOGIC

P.-L. Curien ENS-CNRS, visiting scientist ate DEC SRC (1-7/92).

Recently the subject of games has arisen (actually come back) from quite
different sources and perspectives at the same time. I am aware of works
or talks by Blass, Joyal (old and recent), Lafont-Streicher and De Paiva
(recent, "abstract"), Coquand, Lamarche, and Abramsky-Jagadeesan (more
recent).

I contribute here to this convergence.  What follows is my own, but owes
much to thoughts of Franc,ois Lamarche. It came to me while searching to
integrate Cartwright-Felleisen's decision trees (POPL 92) with the
sequential algorithms of myself and Ge'rard Berry (1978).

The result which I want to announce here is the following:

I do have an interpretation of the following connectives:
- tensor product,
- linear implication,
- of course,
- with,

in terms of concete data structures and sequential algorithms, that has


5 Jun 1992 21:29

### proofnets/graph theory (retore)

Date: Thu, 4 Jun 92 13:57:18 -0700
To: linear@...

I have proved an abstract graph theoretical
result which has the following straight forward corollaries:

the splitting times property even with the mix-rule.
(a la Girard sequentialization, even with mix)

the splitting par property
(a la Danos sequentialization)

So this unifies some hitherto unrelated results.

It says a bit more when working with mix.
Assume all conclusion are times.  Then for any  of
this times conclusions there exists a splitting times and a
feasible path leading to this splitting times.
Also:  assume t is a splitting times, with other splitting times
on his right; then there exists among them at least one which is
connected by a feasible path to t.

The combinatorial argument consist in studying agregates of
complete bipartite graphs, ie edge coloured graph such that
each colour is a complete bipartite graph, and direct paths, ie paths
using at most one edge of each colour.

A paper has been written,  and his to be submitted
(when polished )to a  combinatorics journal.



8 Jun 1992 21:48

### INFORMAL WORKSHOP June 15

Date:  Fri,  5 JUN 92 17:42 N
To: LINEAR@...

This is to recall that the
IILLW
(second linear-logic workshop,Siena, Italy)
will be on June 15 (arrival) to June 18(departure).
Partecipants have only to pay for accomodation
and meals at the Certosa di Pontignano (approx. 50 USD for
full board).
ursini@...

Aldo Ursini,
Department of Mathematics
University of Siena
53100 SIENA, Italy
Phone 0577.286244
Fax   0577.270581
e/mail URSINI@...


8 Jun 1992 21:55

### translations of classical into LL

Date: Mon, 8 Jun 92 10:32:46 +0200
To: linear@...

In their important paper in LICS'91, Lincoln, Scedrov and Shankar give
a translation of a contraction- and cut-free system for implicational
intuitionistic logic into a fragment of propositional linear logic.

In the short LaTeX abstract below, we present how, somewhat in a similar
spirit, we can give a translation of the full propositional classical
logic into the full propositional linear logic without exponentials.

Simone Martini e Andrea Masini
Dipartimento di Informatica,
Universita' di Pisa, Italy.
===========================================================
\documentstyle{article}
\newtheorem{pro}{Proposition}
\newtheorem{de}{Definition}
\newtheorem{teo}{Theorem}

\newcommand{\n}{\mbox{$\neg$}}
\newcommand{\sse}{\mbox{$\equiv$}}
\newcommand{\vel}{\mbox{$\vee$}}
\newcommand{\et}{\mbox{$\wedge$}}
\newcommand{\imp}{\mbox{$\supset$}}

\newcommand{\ms}[2]{
\begin{array}{c}


10 Jun 1992 18:15

### Linear logic question

Date: Wed, 10 Jun 92 14:56:31 BST

Define the formulae of linear logic as usual:

atoms			X
linear formulae		A, B ::=  X | (A -o B) | !A

Define also two subsets of formulae:

standard formulae	A*, B* ::=  X | (A$-o B*) lax standard formulae A$     ::=  A* | !A*

Standard form only allows ! to the left of -o, while lax standard form
optionally allows ! at the beginning.  Let Gamma$range over sequences of lax standard formulae. I conjecture that the following is the case: If Gamma$ |- A$and A$ begins with !
then each formula in Gamma\$ begins with !

I'd be grateful if anyone could verify or disprove this conjecture,
or point me to related work.  Thanks,  -- Phil

-----------------------------------------------------------------------
Department of Computing Science                    tel: +44 41 330 4966
University of Glasgow                              fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND



11 Jun 1992 20:18

### Advanced School on LOGIC and ARTIFICIAL INTELLIGENCE

Date: Thu, 11 Jun 92 17:20:09 +0200

Advanced School on LOGIC and ARTIFICIAL INTELLIGENCE
Udine (Italy), September 28 - October 9, 1992

Organized by:

AI*IA 	- Associazione Italiana per l 'Intelligenza Artificiale
AILA		- Associazione Italiana di Logica e sue Applicazioni
GULP	- Gruppo ricercatori e Utenti di Logic Programming

Hosted by CISM - International Center for Mechanical Sciences

School coordinators:
G. Amati - Fondazione Ugo Bordoni, Roma
D. Pedreschi - University of Pisa

PRELIMINARY PROGRAM

F. PARLAMENTO - University of Udine (Italy)
Proof theory and sequent calculi

M. ABRUSCI - University of Rome (Italy)
Linear Logic

S. VALENTINI - University of Padova (Italy)
Sub-structural logics and many-valued semantics

J. van BENTHEM - University of Amsterdam (The Netherlands)


18 Jun 1992 19:34

### translating classical to linear logic (338 lines)

Date: Wed, 17 Jun 92 15:44:10 +0200

Yes, it's me again.
Sorry to bother all of you!
I received several new answers for my request of a simple embedding
of Classical Logic inside Linear Logic.

I mail them to the net because they could be of general interest.

From: stefano@... ( Stefano Berardi )
Date: Mon, 25 May 92 15:55:54 +0200

A quick question to linear people:

what is the simplest interpretation of First Order Classical Logic in Linear
Logic known up to now?
Of course I heard of several of them, but I found all of them a bit tricky.
I consider only complete interpretations, i.e. mapping:

Phi: {First Order Classical Formulas} -> {First Order Linear Formulas}

such that A is a classical theorem iff Phi(A) is a linear theorem.
Please answer me, not to the net, since I suppose the argument be widely
known, except by me!

S. Berardi

>From murthy@... Wed May 27 14:52:24 1992

Hi, Stefano,


20 Jun 1992 00:22

### linear decorations

Date: Thu, 18 Jun 1992 17:30:10 +0200
X-Organisation: Faculty of Mathematics & Computer Science
University of Amsterdam
Kruislaan 403
NL-1098 SJ Amsterdam
The Netherlands
X-Phone:        +31 20 525 7463
X-Telex:        10262 hef nl
X-Fax:          +31 20 525 7490
To: linear@...

OPTIMAL LINEARIZATION OF INTUITIONISTIC DERIVATIONS
===================================================
(*Abstract*)

V.Danos, J-B.Joinet & H.Schellinx

Technically speaking, we construct a minimal (proof by proof) embedding
of intuitionistic logic into linear logic.
There exist uniform translations from classical (intuitionistic) sequent
calculi to (intuitionistic) linear sequent calculus. A common defect, however,
is their plethoric use of exponentials, which generally prohibits any
computational interpretation.
The purpose of the work presented here, is to produce linearizations
(we call them "decorations") of derivations given in (some version of) sequent
calculus such that :
1/ the "skeletons" of original proofs are preserved,
2/ each exponential in the resulting linear proof is there for a
"good" (= necessary) reason, i.e. because of some instance of a contraction
or weakening rule somewhere in the proof.