Abstract : Focusing and selection are techniques that shrink the proof search
space for respectively sequent calculi and resolution. To bring out a
link between them, we generalize them both: we introduce a sequent
calculus where each occurrence of an atom can have a positive
or a negative polarity; and a resolution method where each literal,
whatever its sign, can be selected in input clauses. We prove the
equivalence between cut-free proofs in this sequent calculus and
derivations of the empty clause in that resolution method. Such a
generalization is not semi-complete in general, which allows us to
consider complete instances that correspond to theories of any logical
strength. We present three complete instances: first, our framework
allows us to show that ordinary focusing corresponds to
hyperresolution and semantic resolution; the second instance is
deduction modulo theory and the related framework called
superdeduction; and a new setting, not captured by any existing framework,
extends deduction modulo theory with rewriting rules having several
left-hand sides, which restricts even more the proof search space.
