Computational Complexity of Deciding Provability in Linear Logic and Its Fragments

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.