Decision problems for second-order linear logic

Author

Lincoln, Patrick ; Scedrov, Andre ; Shankar, Natarajan

Author_Institution

Comput. Sci. Lab., SRI Int., Menlo Park, CA, USA

fYear

1995

fDate

26-29 Jun 1995

Firstpage

476

Lastpage

485

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

Keywords

decidability; decision theory; formal logic; programming theory; contraction; decision problem; first order quantifiers; intuitionistic second order fragment; multiplicative connectives; multiplicative linear logic; propositional multiplicative linear logic; second order linear logic; second order propositional quantifiers; second-order linear logic; structural rules; undecidability; weakening; Computational modeling; Computer science; Computer simulation; Ear; Functional programming; Laboratories; Linearity; Logic programming; Petri nets; Polynomials;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on

Conference_Location

San Diego, CA

ISSN

1043-6871

Print_ISBN

0-8186-7050-9

Type

conf

DOI

10.1109/LICS.1995.523281

Filename

523281