Logic in Computer Science (LICS 1995)

Paper: Decision Problems For Second-Order Linear Logic (at LICS 1995)

Authors: Patrick Lincoln Natarajan Shankar Andre Scedrov

Abstract

The decision problem is studied for fragments of second-order linear logic without modalities. It is shown that the structural rules of contraction and weakening may be simulated by second- order propositional quantifiers and the multiplicative connectives. Among the consequences are the undecidability of the intuitionistic second-order fragment of propositional multiplicative linear logic and the undecidability of multiplicative linear logic with first-order and second-order quantifiers.

BibTeX

  @InProceedings{LincolnShankarScedr-DecisionProblemsFor,
    author = 	 {Patrick Lincoln and Natarajan Shankar and Andre Scedrov},
    title = 	 {Decision Problems For Second-Order Linear Logic},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {476-485},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }