Subject: Proof search strategies in linear logic
From: Tanel Tammet <[email-masked]>
To: [email-masked]
Date: Thu, 25 Feb 93 16:45:18 +0100

--text follows this line--

This message announces the availability of the paper
"Proof search strategies in linear logic", currently in
print as a Chalmers Univ. of Tech. Programming Methodology
Group report nr 70. It is also submitted for journal publication.
You can get it by anonymous ftp or mail, see the following.

Some people might have seen an earlier draft of this paper.
The new version is a complete rewrite.

---------------------------------------------------------------

             Proof search strategies in linear logic
                         
                        Tanel Tammet

               Department of Computer Sciences
              Chalmers University of Technology
                 41296 G"oteborg, Sweden

               email: [email-masked] 

                         Abstract

We investigate methods for automated theorem proving in full 
propositional linear logic. Both the ``bottom-up'' and ``top-down''
(resolution) proof strategies are analyzed -- various modifications
of sequent rules and efficient search strategies are presented along
with the experiments performed with the implemented theorem provers.  

----------------------------------------------------------------

The .dvi version of the file is available by anonymous ftp from
ftp.cs.chalmers.se from the directory pub/papers as llsearch.dvi.Z 
Do not forget to set the mode to binary!
The following is a sample ftp session:

    %ftp ftp.cs.chalmers.se
    Name=anonymous  
    >cd pub/papers
    >binary
    >get llsearch.dvi.Z
    >bye
    
Now you are back at your home directory. Do: uncompress llsearch.dvi 
Contact me for the already-printed version.

You can also get the provers, in Scheme or C or the SUN4 executable.

Regards,
	Tanel Tammet


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Fri, 26 Feb 93 13:22:45 +0100
From: Tanel Tammet <[email-masked]>
To: [email-masked]
Subject: The .dvi file for the proof search paper corrected
Sender: [email-masked]
--text follows this line--

This message announces that the .dvi file of the paper
"Proof search strategies in linear logic" available by
anonymous ftp from ftp.cs.chalmers.se as pub/papers/llsearch.dvi.Z
has been replaced by a new version, which does not use
uncommon fonts any more, and should thus be portable.

Many thanks for all the people who reported that they could
not print out the previous version of llsearch.dvi, as
it contained a special font stmaryrd with the inverse ampersand.
I hope the new version is portable.

To compensate for the mess, I have made the sequent calculus
bottom-up prover for full propositional linear logic available
by anonymous ftp from ftp.cs.chalmers.se as pub/provers/linseq.tar.Z

It contains both the C version and the Scheme version of the
prover. Read the file README to get information about compiling
the C version by doing: make linseq 

Do not forget to set the mode to binary!
The following is a sample ftp session to get the prover:

    %ftp ftp.cs.chalmers.se
    Name=anonymous  
    >cd pub/provers
    >binary
    >get linseq.tar.Z
    >bye
    
Now you are back at your home directory. Do: uncompress linseq.tar
After that do: tar xvof linseq.tar 
After that read README

Regards,
	Tanel Tammet


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
From: [email-masked] ( Dr G Bellin tel 2-76933)
Date: Tue, 9 Mar 93 18:39:25 GMT
To: [email-masked]
Subject: (short) paper available
Sender: [email-masked]
--text follows this line--

The following paper
     LC-nets.dvi.Z
is available by anonymous ftp from
     theory.doc.ic.ac.uk
The file is in the directory
     /papers/Bellin
use uncompress to obtain the dvi-files.

A few comments on the content:

1. The paper LC-nets provides a solution to a question in Girard [1991]
`A new constructive logic: classical logic'. Recall that LC formalizes
classical logic and has canonical translations into LJ and also LL.

To see why this is not just a straightforward adaptation of usual
LL-proof-nets to LC, notice that a sequent
                   |- A1,...,An ; Q
has an interpretation of the form
                   ! X1 times ... ! times Xn  |-  ! X.
Thus to find a system of proof-nets for LC means to produce a method
to remove a specific class of !-boxes.

2. To do this we introduce the notion of privileged empire; the fact that
such a simple modification of the notions of kingdom and empire is enough
to do the job is another sign of the utility of (what one could call)
the `quasi-topology of subnets'. A detailed presentation of the relevant
results is in the paper by Bellin and van de Wiele `Proof-nets and
typed lambda -calculus' which will be available very soon here (as other
EEC cooperative projects, its completion takes longer than expected).

I would like to know recent results in the area of LC or LU
(I have not recently received any announcement on the topic
from the [email-masked] mailing list).

Gianluigi Bellin


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
To: [email-masked]
Organization: Tver State University
From: [email-masked] (Taitslin M.A.)
Date: Mon, 22 Mar 93 10:13:24 +0300 (MSK)
Subject: Simplified NP-Completeness of MLL
Sender: [email-masked]
--text follows this line--

One of the well known recent results is the Kanovich' theorem
about NP-completeness in linear logic.
I give proof of NP-completeness of the problem of provability
of Horn sequents of linear logic.
This proof uses one fact:
the Horn sequent is provable iff the right part of the
sequent is obtained from the left one consequtivelly applying in some order
all the implications (as defining relations for a commutative semigroup) to 
available letters (forming a word of the free commutative semigroup).
We consider the problem:
To partition a sequence a1,..,a3m of 3m positive
integer numbers having the sum am into m triples, the sum of each of which
is equal to a.
We use variables x,(v1),...,(vm),(u1),...,(um), (z1),...,(z3m).
Let the left part of the sequent be

  ma    3
 x  (u1) (z1)...(z3m)

                 a1         a1
       ((u1)(z1)x   --> (v1)  )
       ..........................
                  a3m          a3m
       ((u1)(z3m)x     --> (v1)    )

            a          3
       ((v1)   --> (u2) )
       ...........................
       ...........................

                 a1         a1
       ((um)(z1)x   --> (vm)  )
       ........................................
                  a3m          a3m
       ((um)(z3m)x     --> (vm)    )

            a          3(m-1)       3(m-1)    m-1        m-1 ma(m-1)
       ((vm)   --> (u1)      ...(um)      (z1)   ...(z3m)   x       )

Let the right part of the sequent be

     (m-1)a       (m-1)a
 (v1)      ...(vm)

It is obvious that this sequent is provable iff the sequence a1,..,a3m
can be partitioned.

Taitslin M.A.
---------------------------------------------------

Administrator's Note: 

As announced earlier on the linear list, M. Kanovich 
has since improved his results.  Also, in a paper announced last 
year on the linear list by myself and Winkler, we show that 
NO propositions are needed for a similar encoding of 3-Partition.
That is, the constant-only mulitplicative fragment of linear logic 
is also NP-Complete.  A paper on the subject is available by 
anonymous FTP from cs.stanford.edu as /pub/lincoln/comult-npc.dvi.Z


Patrick LincolnReturn-Path: <[email-masked]>
Date: Thu, 11 Mar 93 18:46:22 BSC
From: [email-masked] (Mamede Lima Marques - POS_MAT)
Subject: X BRAZILIAN CONFERENCE ON MATHEMATICAL LOGIC
To: [email-masked]
Sender: [email-masked]
--text follows this line--

                        CONFERENCE ANNOUNCEMENT

         X BRAZILIAN CONFERENCE ON MATHEMATICAL LOGIC  -EBL93

                   Itatiaia, Rio de Janeiro, Brazil
                            17-21 May, 1993

Sponsored by: Center for Logic, Epistemology and the History of Science,
              University of Campinas, and
              Sociedade Brasileira de Logica

Program Committee:
              Walter Alexandre Carnielli, UNICAMP
              Jos'e Alexandre D, Guerzoni, UNICAMP
              Luis Carlos P. D. Pereira, UFRJ
              Vera Vidal, UFRJ

Partial list of speakers:
             Newton C. A. da Costa, USP, Brazil
             Paul Gochet, Univ. de Liege, France
             Goeran Sundholm, Unov. of Nijmegen, Holland
             Luis Farinas del Cerro, IRIT, France
             Oswaldo Chateaubriand, PUC\RJ, Brazil
             Francisco Doria, UFRJ, Brazil
             Paulo A. Velloso, PUC/RJ, Brazil
             Antonio M. A. Sette, UNICAMP, Brazil
             Itala M. L. D'Ottaviano, UNICAMP, Brazil
             Luis.P. de Alcantara, UNICAMP, Brazil
             Michael Wrigley, UNICAMP, Brazil
													Carlos A. Lungarzo, UNICAMP, Brazil

You are cordially invited to  participate in the EBL93, whose
topics include: 

             Classical Logic -Proof Theory
             Classical Logic -Model Theory
             Logic and Computer Science
             Set Theory
             Non -Classical Logics- Theoretical Aspects
             Applications of Non-Classical Logics
             Philosophical Aspects of Logic

Correspondence should be sent to:

             Maria das Gracas P. Sanches, Secretary-EBL93
             Center for Logic and Epistemology
             C. P. 6155, 13081-970, Campinas , SP, Brazil
            
             fax: +(55 192)39 32 69
             e-mail: [email-masked]

--------------------------------------------------------------


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Organization: Tver State University
From: [email-masked] (Taitslin M.A.)
Date: Tue, 30 Mar 93 16:30:27 +0300 (MSK)
To: [email-masked]
Subject: Question on NP-Completeness
Sender: [email-masked]
--text follows this line--

 Can anybody send me a proof of NP-completeness of the following problem:
  
      has sequent      a(v1->w1)...(vn->wn) !- b
      where a,b,v1,...,vn,w1,...,wn are elements 
      of the free commutative   semigroup with two generators
      a proof in MLL?
 
 Please send answer to the address :
 @techno.fuug.fi:@sovcom.kiae.su:[email-masked]
 
 M.A.Taitslin
 Tver State University, Russia


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Organization: Tver State University
From: [email-masked] (Taitslin M.A.)
Date: Fri,  2 Apr 93 12:46:13 +0300 (MSK)
To: [email-masked]
Subject: Answer to Question on NP-Completeness
Sender: [email-masked]
--text follows this line--

 This is an answer to my question distributed some days ago. 
 Let a1,...,a3m be positive integers each less then a. Let
 a1+...+a3m=ma. The sequent

   9a  3a   a-a1 a1      3a   a-a3m a3m   2a a   9a m-1      2a a
  y  (y  ->z    y  )...(y  ->z     y   )(z  y ->y  )     |- z  y
  
is provable in MLL iff a1,...,a3m can be divided on m triples with
sum a.
Thus the problem
      have sequent      a(v1->w1)...(vn->wn) !- b
      where a,b,v1,...,vn,w1,...,wn are elements 
      of the free commutative   semigroup with two generators
      a proof in MLL?
 is NP-complete.

 @techno.fuug.fi:@sovcom.kiae.su:[email-masked]
 M.A.Taitslin
 Tver State University, Russia


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Mon, 5 Apr 93 07:58:35 EDT
From: [email-masked] (Mitsu Okada)
To: [email-masked]
Subject: A paper available for anonymous FTP.
Sender: [email-masked]
--text follows this line--

A paper "Mobile Linear Logic as a Framework for Asyncronous and
Syncronous Mobile Communication Process Calculi" (by M. Okada) is available
through anonymous FTP, at triples.math.mcgill.ca, under the directory
pub/okada. Use "anonymous" for the user's name and your address for
the password, as usual. 

Abstract: We propose a variant of second order linear logic for a
framework of mobile communication process calculi. In the proposed
mobile linear logic language the second order terms are identified
with the first order terms; With our mobile language we could
express not only a traditional logical sentence, such as Love(Tom,
Mary) "Tom loves Mary", but also a sentence such as Love(Tom, Love)
"Tome loves the idea of love", or Love(God, \lambda x \forall y
Love(x,y)), "God loves the idea of loving everyone", or such a predicate
on x as Love(x, \lambda y Love(x,y)), i.e., predicate "x loves x's
own love".

We use our mobile linear logic framework for the
proof-search-as-computation paradigm based on linear logic, 
proposed by D. Miller, Andreoli-Pareschi and Saraswat-Lincoln.
More directly, we consider the setting similar to Kobayashi-Yonezawa.
The main differences of our proposed framework from the others
include, among others, the following; (1) We identify the "unprovable" (hence,
maybe infinite) proof trees with the process schedules. (in this way,
the finite and infinite processes are both treated in a uniform way
in our formalism.), in contrast to the use of "provable" finite
proof trees by the other authors.  (2) The strength of mobile
message communications is classified in terms of the traditional
proof-theoretic notions, by the use of the well-known hierarchy of 
comprehension rules and of nested  implications. (In particular, the
employment of our mobile language accommodates a strong mobile message
passing, which cannot be realized by the traditional higher order
languages, such as the one used by Saraswat-Lincoln).  

We give a general framework of the mobile linear logic and 
its subsystems which have direct meaning as a mobile
process calculus. The main purpose of this paper is to give
a basic semantic and proof-theoretic analysis of this framework.
The traditional Tarski-style
completeness theorem is now restated as the equivalence
between consistency of a specification formula and existance
of a safe (generalized) schedule. The phase semantic analysis
of the general framework is also given. A syncronous communication
is characterized by specifying a proof search strategy in the
asyncronous communication based-proof system.


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Thu, 8 Apr 93 12:39:38 +0200
To: [email-masked]
From: [email-masked]
Subject: Linear Logic and Exceptions
Sender: [email-masked]
--text follows this line--

                                   Linear Logic and Exceptions
                                   -----------------------------------

Extended abstract

A semantic network is a structure for representing knowledge as a pattern
of interconnected nodes and edges. The nodes represent concepts or
properties of a set of individuals, whereas the edges represent relations
between concepts. The network can be viewed as a hierarchy of concepts
according to levels of generality. A more specific concept is said to
inherit informations from its subsumers.  The formalization of human
reasoning asks for some kind of uncertain knowledge represented in semantic
networks as default edges: for example, we expect the concept of bird to be
more specific than the concept of flying object, even if some species
cannot fly. Generally speaking, we consider networks with default and
exception edges, dealing respectively with defeasible and exceptional
knowledge. Nonmonotonic logics were developed in the last decade in order
to represent defaults and exceptions in a logical way: the set of inferred
grounded facts is the set of properties inherited by concepts. In this
paper, we investigate the problem of formalizing inheritance in semantic
networks with default and exception links in a standard logic, namely
linear logic. This research was undertaken after a short paper of Girard
(1992, J. of Logic and Computation) as he noticed that "the consideration
of weird classical models [in nomonotonic logics] definitely cuts the
bridge with formal systems but also with informal reasoning" and that "the
surprising ability of linear logic to encode various abstract machines
indicates that much more can be done following this line". 
We first present a few examples whose intended meanings is to point out
graphically what we expect of such semantic networks. These examples are
described later in a default logic way and in a linear logic way. We
consider the following taxonomic networks in this paper.
A TNE (Taxonomic Network with Exceptions) is defined as a triple N=<N,-->,
- >> such that:
		. N is a finite set of nodes
		. -->, - >  are two functions that associate to each node of N a set of
nodes of N
	with the two following constraints:
		. <N,-->> is an oriented graph without cycles.
		. Let R be the set of roots of <N,-->>, then R and - >(N) are disjoint. 
 The second section concerns linear logic. We show that linear logic
formalizes semantic networks with defaults and exceptions. We present the
fragment of linear logic in which these networks can be axiomatized. It
includes mainly the multiplicative fragment of linear logic. The rest is
devoted to the modelisation of these networks, namely taxonomic linear
theories. It is then proved that inferences correspond to a subset of
provable sequents, simple sequents. Finally, we relate such proofs to nets
via pseudo-nets. A pseudo-net is a finite graph composed of coloured
vertices and of coloured oriented edges. Pseudo-nets constructed from
standard proofs of simple sequents are called nets. It is proved that a
pseudo-net is a net if and only if its orientation is an ordering. The
third section is devoted to a presentation of default logic. We recall
theorems that link the computation of extensions to default sets (sets of
generating defaults) and define a fragment axiomatizing our taxonomical
networks. The fourth section is devoted to the proof of the equivalence
between extensions in taxonomical default theories and simple sequents in
taxonomical linear theories. Improvements are finally discussed.

Christophe Fouquere, Jacqueline Vauzeilles
LIPN-CNRS URA 1507
Universite Paris-Nord
93430 Villetaneuse
e-mail: {cf,[email-masked]


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Mon, 26 Apr 93 17:26:48 +0200
From: Sanjiva Prasad <[email-masked]>
To: [email-masked]
Subject: Mix Rule and Girardian Turnstile
Sender: [email-masked]
--text follows this line--

One request and one question:

1. The request is for the "official" LaTeX macro for the Girardian turnstile.

2. The question is about the MIX rule

	/-  A      /- B
        ---------------
           /- A par B

that Girard mentions.  What are the consequences of having such
a rule (other than   A tensor B  -o  A par B)?  Has anyone used
the MIX rule to explain parallel composition of process calculi such
as CCS, particularly the way the parallel composition operator
(CCS |) is used to represent both connected and unconnected concurrency?

How would the MIX rule be rendered in LU?  Am I right in 
conjecturing the following?

	; Gamma' /- Delta' ; A		; Gamma' /- Delta' ; B
	------------------------------------------------------
			; Gamma' /- Delta' ;  A par B

Thanks in advance for any insights.

- Sanjiva	([email-masked])

PS: I'm quite new to linear logic, and I'm interested more in
proof assignment than in proof search.