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.
Guillaume Burel. Linking Focusing and Resolution with Selection. 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), Aug 2018, Liverpool, United Kingdom. pp.9:1-9:14, ⟨10.4230/LIPIcs.MFCS.2018.9⟩. ⟨hal-01670476v3⟩