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.