**Friday 18 March 2016**, 10:30: Linking Focusing and Resolution with Selection, Guillaume Burel (ENSIIE).

Focusing and selection are techniques that shrink the proof search
space for respectively sequent calculi and resolution. We generalize
both of them: we introduce a sequent calculus where each
*occurence* of an atom can be positive or negative; and a
resolution method where each literal, whatever its sign, can be
selected. We prove the equivalence between cut-free proofs in this
sequent calculus and derivations of the empty clause in that
resolution method. Of course, such a generalization is not
semi-complete in general. We present three complete instances: first,
our framework allows us to show that usual focusing corresponds to
semi-ordered hyperresolution; the second instance is
deduction modulo theory; and a new setting extends deduction
modulo theory with rewriting rules having several left-hand sides,
therefore restricting even more the proof search space.