1 Search Results for "Burel, Guillaume"


Document
Linking Focusing and Resolution with Selection

Authors: Guillaume Burel

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)


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 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.

Cite as

Guillaume Burel. Linking Focusing and Resolution with Selection. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{burel:LIPIcs.MFCS.2018.9,
  author =	{Burel, Guillaume},
  title =	{{Linking Focusing and Resolution with Selection}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.9},
  URN =		{urn:nbn:de:0030-drops-95917},
  doi =		{10.4230/LIPIcs.MFCS.2018.9},
  annote =	{Keywords: logic in computer science, automated deduction, proof theory, sequent calculus, refinements of resolution, deduction modulo theory, polarization}
}
  • Refine by Author
  • 1 Burel, Guillaume

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 automated deduction
  • 1 deduction modulo theory
  • 1 logic in computer science
  • 1 polarization
  • 1 proof theory
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail