headers
Stefano Berardi | 3 Jun 1992 15:17
Picon
Favicon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gerard Huet | 4 Jun 1992 19:18
Picon
Picon
Favicon

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
with Name anonymous and Password your email address.
Then do
binary
cd INRIA/coq
get README
get coq.tar.Z
quit

Now uncompress coq.tar.Z, untar coq, and follow the README instructions.

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@...
(Continue reading)

Permalink | Reply | 0 comments |
headers
curien | 4 Jun 1992 20:38
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
deptang | 5 Jun 1992 21:29
Picon

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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
URSINI%SIVAX.CINECA.IT | 8 Jun 1992 21:48
Picon

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@...
Permalink | Reply | 0 comments |
headers
Andrea Masini | 8 Jun 1992 21:55
Picon
Picon

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.

Comments and remarks are welcome.

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}
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip Wadler | 10 Jun 1992 18:15
Picon

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

-----------------------------------------------------------------------
Philip Wadler                                  wadler@...
Department of Computing Science                    tel: +44 41 330 4966
University of Glasgow                              fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND
(Continue reading)

Permalink | Reply | 0 comments |
headers
pedre | 11 Jun 1992 20:18
Picon
Picon

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
C. Sossai - LADSEB-CNR, Padova

			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)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Stefano Berardi | 18 Jun 1992 19:34
Picon
Favicon

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,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Harold A.J.M. Schellinx | 20 Jun 1992 00:22
Picon
Picon

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.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane