Invariants of proofs in classical logic

Lutz Straßburger, INRIA Sacalay - Île-de-France

LIX, Ecole Polytechnique, Palaiseau

The questions ``What is a proof?'' and ``When are two proofs the same?'' are fundamental for proof theory. But for the most prominent logic, Boolean (or classical) propositional logic, we still have no satisfactory answers.

This is embarrassing not only for proof theory itself, but also for computer science, where classical propositional logic plays a major role in automated reasoning and logic programming. Also the design and verification of hardware is based on classical Boolean logic. Every area in which proof search is employed can benefit from a better understanding of the concept of proof in classical logic, and the famous NP-versus-coNP problem can be reduced to the question whether there is a short (i.e., polynomial size) proof for every Boolean tautology.

Usually proofs are studied as syntactic objects within some deductive system (e.g., tableaux, sequent calculus, resolution, ...). Invariants for proofs are mathematical objects that abstract away from the syntax, in order to be able to distinguish proofs, in the same sense as homology groups serve as invariants to distinguish topological spaces. Examples of invariants for proofs are proof nets, logical flow graphs, combinatorial proofs, and atomic flows.

The task for this internship is to study these invariants, in particular, compare their behaviour with respect to proof normalization, and investigate correctness criteria that allow to recover the full syntactic proof from the invariant.

Basic knowledge in logic and proof theory.

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