back to Lutz Straßburger

Lutz Straßburger

Research Topics and Open Problems


Every research field lives from its open problems. If there are no open problems left, it dies.

Currently, I am working in structural proof theory, which is a very vivid and active field.  In the following I list some of the open problems in the field. One can consider it as a resource for topics for Internship/Bachelor's/Master's/PhD/Post-doctoral work. Note that the list is by no means exhaustive. You might also want to have a look at the list of research topic and open problems collected by Alessio Guglielmi and at Kai Brünnler's list of open problems. In fact, you should consult these lists since I avoided unnecessary repetitions.

1. Topics for Internships / Master's Theses

This is a list of problems already tailored to be a topic for an internship or a Master's thesis. They are suited for students who have not seen any proof theory before. All you should bring is an interest in working theoretically and some basic knowledge in logic.

1.1  Proof search with quantifiers in deep inference

The proof-theoretical foundations for proof search in first-order and higher-order logic are provided by Gentzen's sequent calculus. For implementation, a unification procedure has been put on top of that.

The problem in implementing proof search is deciding at what point the unification should happen. The sequent calculus tells us to instantiate a variable in the moment the rule for the existential quantifier is applied. However, at that moment, the machine has no way to know with what the variable should be instantiated. Only later when the proof search reaches an identity axiom, this knowledge is revealed (of course, the human reasoner always has the possibility of making a clever guess).

In practical implementations this problem is usually solved by laziness. One keeps a "hole" in the proof and postpones the unification to the very end of the proof. While this clearly works well for practical purposes, it is a disaster for the theory of proofs, because there is no well defined notion of "proof object". There are only meta-language descriptions.

The notion of deep inference that can solve that problem in a very elegant way by simply postponing the application of the rule that removes the existential quantifier. This is easily possible by working inside the formula, which is not possible with the sequent calculus which has to remove the quantifier in order to get access to the formula inside in the first place. This can give a proper proof theoretical treatment to the implementations.

An internship or master's thesis could be developped around the following specific tasks:

Web page for this internship

1.2  Normal forms for classical logic proofs in deep inference

Deep inference is a recently developped paradigm for presenting deductive systems. It has successfully be applied for varios logics, like classical logic, linaer logic, intuitionistic logic and modal logics. The novelty is that inference rules are allowed to be applied like rewrite rules deep inside formulas. This is not possible with shallow inference systems like sequent calculus or natural deduction.

The new freedom in the design of inference rules has a drawback: The usual techniques for obtaining important properties, like cut elimination, break down. For this reason new techniques, like splitting and decomposition have been developped.

The task for this internship is to apply these new methods to the deep inference system SKS for classical logic, and relate the cut elimination proof obtained in this way to cut elimination in the sequent calculus and in proof nets.

Web page for this internship

1.3  Proof nets and deep inference for linear logic

Superficially, proof nets and deep inference seem to be to opposite approaches towards the problem of the identity of proofs (When are two proofs the same?): Proof nets are graph-like presentations of proofs that quotient away trivial rule permutations in the sequent calculus, and by this make more proof identification than the sequent calculus. On the other hand, in a deep inference system rules have a much finer granularity which allows even more permutations than the sequent calculus, and therfore there are less proof identification than the sequent calculus.

However, the finer granularity of inference rules allows a finer analysis of the inner structure of proofs which then can lead to new notions of proof nets which are independent from the sequent calculus. This mean that we now can avoid constructs like boxes in proof nets which are there because the sequent calculus makes use of some global information. This is particularly visible in multiplicative exponential linear logic (MELL), where the promotion rule is global in the sequent calculus and local in the deep inference system.

The problem for this internship is to exploit this locality and design proof nets without boxes for MELL.

Web page for this internship

1.4  Proof nets for modal logics

Here we can say exactly the same as for the previous problem. The only difference is that there are, so far, no proof nets for modal logics. Not even with boxes. But there are local deep inference systems for modal logics.


1.5  Deep inference for temporal logics

Here we are one step behind. We don't even have a deep inference system for temporal logics. Neither do we in the sequent calculus nor in natural deduction.

This means that there is a huge playground. Just pick you favorite temporal logic, and come up with a deductive system for it.

Web page for this internship

2. Open Problems

Here is a list of open problems for which I do not dare to give an estimate for their difficulty. All I can do is to give a warning about the first two: I tried to solve them myself but was not successful...

2.1  The decidability of MELL

MELL is the multiplicative exponential fragment of linear logic, and it is not known whether provability is decidable or not. I believe it is. And I believe that the best approach for proving that is to use the tree-automata-version of vector addition systems with states (VASS). Roughly speaking, these are finite state automata where the transitions are labelled by vectors over the integers. They have been used to show the decidability of the reachability in Petri-nets. The problem is to develop the same technology for the tree-VASS.

2.2  The equivalence of BV and Pomset-logic

Pomset logic is a natural extension of multiplicative linear logic by a non-commutative self-dual connective. It has been discovered by Christian Retoré who presented it in terms of proof nets and a simple graph-theoretic correctness criterion.
 
System BV is a natural extension of multiplicative linear logic by a non-commutative self-dual connective. It has been discovered by Alessio Guglielmi who presented it in terms of the calculus of structures.

It should be clear what my opinion about the problem is. In fact, there is only a little lemma missing...

2.3  Proof nets for the quantifiers

How can the quantifiers be incorporated in proof nets? Note that asking this question means at the same time asking the question about the essence of a proof with quantifiers. This might be the place where structural proof theory (which is mostly concerned with propositional logics) meets the other areas of proof theory: constructivism, logical complexity, and ordinal analysis. I guess that a good starting point are Dale Miller's expansion trees. But as usual in proof theory, the problems come with cut elimination.

2.4  Close the gap between proof nets and deductive systems

Deductive systems are based on inference rules, and usually there is a lot of redundancy involved in the order in which the rules are applied. Proof nets (should) completely abstract away from this redundancy. Although one should be able to read back a formal proof in a deductive system from a correct proof net, we are not able to perform the search for the proof directly in the proof net setting. Is there a way of closing this gap, i.e., is there a formalism that abstracts away from unnecessary buraucracy, and is at the same time suited for proof search? (these are the objects that Alessio Guglielmi calls "deductive proof nets".)

2.5  A categorical axiomatization for classical logic

to be completed

2.6  ...

to be completed


  Last update:  September 25, 2006            Lutz Straßburger