Decision Problems for Second-Order Linear Logic

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 quanti ers 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 rst-order and second-order quanti ers.

• Type: Conference
• Year: 1995
• Where: LICS
• Authors: Patrick Lincoln, Andre Scedrov, Natarajan Shankar
• Keywords: Automated Reasoning, LICS 1995, Multiplicative Linear Logic, Second-order Linear Logic, Second-order Propositional Quanti