Proof systems for intuitionistic logic

Roy Dyckhoff ( School of Computer Science, University of St Andrews. )

We survey the wide range of proof systems proposed for intuitionistic logic, emphasising the differences and their design for different purposes, ranging from ease of philosophical or other semantic justification through programming language semantics to automated reasoning. In particular we will mention (and perhaps even cover) a basic Hilbert-Frege system, Gentzen's natural deduction system NJ, its modification LJ (aka G1) systems of Gentzen, the G3-style systems of Ketonen and Kleene, the multi-succedent calculus of Maehara, the focused calculi LJQ and LJT of Herbelin motivated by ideas of linear logic, the depth-bounded calculus G4ip of (independently) Vorob'ev, Hudelmaier and myself, the resolution calculus of Mints, the labelled calculus of Negri, and the deep inference calculus of Brünnler.  [Some of my work on LJT was joint work with Luis Pinto; some of that on LJQ was joint work with Stéphane Lengrand.]