Linking Focusing and Resolution with Selection

Guillaume Burel 1, 2, 3, 4
2 METHODES-SAMOVAR - Méthodes et modèles pour les réseaux
SAMOVAR - Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux
3 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-01670476
Contributor : Guillaume Burel <>
Submitted on : Friday, April 27, 2018 - 12:12:21 PM
Last modification on : Wednesday, December 4, 2019 - 1:30:03 PM

File

lipics.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

192

Files downloads

332