Lics

IEEE Symposium on Logic in Computer Science

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

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 Symposium on Logic in Computer Science (LICS 1995)},
 year =	 {1995},
 month =	 {June}, 
 pages = {476--485},
 location = {San Diego, CA, USA}, 
 publisher =	 {IEEE Computer Society Press}
 }