Return-Path: <@Sunburn.Stanford.EDU:tammet@cs.chalmers.se> Date: Thu, 25 Feb 93 16:45:18 +0100 From: Tanel Tammet To: linear@cs.stanford.edu Subject: Proof search strategies in linear logic Sender: lincoln@cs.stanford.edu --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: tammet@cs.chalmers.se 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:tammet@cs.chalmers.se> Date: Fri, 26 Feb 93 13:22:45 +0100 From: Tanel Tammet To: linear@cs.stanford.edu Subject: The .dvi file for the proof search paper corrected Sender: lincoln@cs.stanford.edu --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:bellin@maths.ox.ac.uk> From: bellin@maths.ox.ac.uk ( Dr G Bellin tel 2-76933) Date: Tue, 9 Mar 93 18:39:25 GMT To: linear@cs.stanford.edu Subject: (short) paper available Sender: lincoln@cs.stanford.edu --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 linear@cs.stanford.edu mailing list). Gianluigi Bellin Return-Path: <@Sunburn.Stanford.EDU:tvegu.tver.su!mat@sovcom.kiae.su> To: linear@cs.stanford.edu Organization: Tver State University From: mat@tvegu.tver.su (Taitslin M.A.) Date: Mon, 22 Mar 93 10:13:24 +0300 (MSK) Subject: Simplified NP-Completeness of MLL Sender: lincoln@cs.stanford.edu --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: Date: Thu, 11 Mar 93 18:46:22 BSC From: mamede@ime.unicamp.br (Mamede Lima Marques - POS_MAT) Subject: X BRAZILIAN CONFERENCE ON MATHEMATICAL LOGIC To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --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: ebl93@ime.unicamp.br -------------------------------------------------------------- Return-Path: <@Sunburn.Stanford.EDU:tvegu.tver.su!mat@sovcom.kiae.su> Organization: Tver State University From: mat@tvegu.tver.su (Taitslin M.A.) Date: Tue, 30 Mar 93 16:30:27 +0300 (MSK) To: linear@cs.stanford.edu Subject: Question on NP-Completeness Sender: lincoln@cs.stanford.edu --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:mat@tvegu.tver.su M.A.Taitslin Tver State University, Russia Return-Path: <@Sunburn.Stanford.EDU:tvegu.tver.su!mat@sovcom.kiae.su> Organization: Tver State University From: mat@tvegu.tver.su (Taitslin M.A.) Date: Fri, 2 Apr 93 12:46:13 +0300 (MSK) To: linear@cs.stanford.edu Subject: Answer to Question on NP-Completeness Sender: lincoln@cs.stanford.edu --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:mat@tvegu.tver.su M.A.Taitslin Tver State University, Russia Return-Path: <@Sunburn.Stanford.EDU:okada@triples.math.mcgill.ca> Date: Mon, 5 Apr 93 07:58:35 EDT From: okada@triples.Math.McGill.CA (Mitsu Okada) To: linear@cs.stanford.edu Subject: A paper available for anonymous FTP. Sender: lincoln@cs.stanford.edu --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:jv@lipn.univ-paris13.fr> Date: Thu, 8 Apr 93 12:39:38 +0200 To: linear@cs.stanford.edu From: jv@lipn.univ-paris13.fr Subject: Linear Logic and Exceptions Sender: lincoln@cs.stanford.edu --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=, - >> 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: . > is an oriented graph without cycles. . Let R be the set of roots of >, 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,jv}@lipn.univ-paris13.fr Return-Path: <@Sunburn.Stanford.EDU:sanjiva@ecrc.de> Date: Mon, 26 Apr 93 17:26:48 +0200 From: Sanjiva Prasad To: linear@cs.stanford.edu Subject: Mix Rule and Girardian Turnstile Sender: lincoln@cs.stanford.edu --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 (sanjiva@ecrc.de) PS: I'm quite new to linear logic, and I'm interested more in proof assignment than in proof search.