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