Proof search with quantifiers in deep inference

Lutz Straßburger, INRIA Futurs

LIX, Ecole Polytechnique, Palaiseau

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

Basic knowledge in logic and proof theory.

The following bibliography is indicative of the kind of papers that will be part of this research effort.

1. Kai Brünnler. Deep Inference and Symmetry for Classical Proofs. Phd Thesis, TU Dresden, 2003.
2. Kai Brünnler. Cut Elimination inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82:51-71, 2006.
3. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. APAL, 51:125-157, 1991.
4. Dale Miller. Forum: A Multiple-Conclusion Specification Logic. TCS 165: 201-232, 1996.

Lutz Straßburger's list of problems
Parsifal's web page
Alessio Guglielmi's web page on deep inference