[Prev][Next][Index][Thread]

Proof search strategies in linear logic



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

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

>From lincoln@Theory.Stanford.EDU Fri Feb 26 17:04:41 1993
>Date: Fri, 26 Feb 93 13:22:45 +0100
>From: Tanel Tammet <tammet@cs.chalmers.se>
>To: linear@cs.stanford.edu
>Subject: The .dvi file for the proof search paper corrected


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

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