Computational Complexity of Deciding Provability in Linear Logic and its Fragments

TL;DR

This paper explores the computational complexity of provability in linear logic and its fragments, presenting new results and highlighting open problems in the field.

Contribution

It provides an original complexity characterization of a linear logic fragment and proposes a new structural approach to studying provability.

Findings

Presented the current state of complexity results for linear logic fragments

Proved a new complexity characterization for a specific fragment

Suggested ideas for a novel structural approach to provability analysis

Abstract

Linear logic was conceived in 1987 by Girard and, in contrast to classical logic, restricts the usage of the structural inference rules of weakening and contraction. With this, atoms of the logic are no longer interpreted as truth, but as information or resources. This interpretation makes linear logic a useful tool for formalisation in mathematics and computer science. Linear logic has, for example, found applications in proof theory, quantum logic, and the theory of programming languages. A central problem of the logic is the question whether a given list of formulas is provable with the calculus. In the research regarding the complexity of this problem, some results were achieved, but other questions are still open. To present these questions and give new perspectives, this thesis consists of three main parts which build on each other: We present the syntax, proof theory, and various approaches to a semantics for linear logic. Here already, we will meet some open research questions. We present the current state of the complexity-theoretic characterization of the most important fragments of linear logic. Here, further research problems are presented and it becomes apparent that until now, the results have all made use of different approaches. We prove an original complexity characterization of a fragment of the logic and present ideas for a new, structural approach to the examination of provability in linear logic.