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

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.

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:

- Develop a proof search strategy for deep inference systems that incorporates the idea described above, and possibly provide a prototype implementation.
- Extend deep inference systems to higher-order quantification (so far, only first-order and second-order have been investigated).

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 internshipSuperficially, 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 internshipHere 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.

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 internshipHere 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...

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.

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...

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...

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.

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".)

Last update: September 25, 2006 Lutz Straßburger