Logic in Computer Science (LICS 1994)

Paper: Proof search in first-order linear logic and other cut-free sequent calculi (at LICS 1994)

Authors: Patrick Lincoln N. Shankar

Abstract

We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Herbrand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for first-order MALL is in NEXPTIME, and first-order MLL is in NP. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability

BibTeX

  @InProceedings{LincolnShankar-Proofsearchinfirsto,
    author = 	 {Patrick Lincoln and N. Shankar},
    title = 	 {Proof search in first-order linear logic and other cut-free sequent calculi },
    booktitle =  {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {282--291},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }