2 Search Results for "Papamakarios, Theodoros"

Document
DOI: 10.4230/LIPIcs.MFCS.2023.74
A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus

Authors: Theodoros Papamakarios

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, for the first time, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Our super-polynomial separation between resolution and cut-free sequent calculus only applies when clauses are seen as disjunctions of unbounded arity; our examples have linear size cut-free sequent calculus proofs writing, in a particular way, their clauses using binary disjunctions. Interestingly, this shows that the complexity of sequent calculus depends on how disjunctions are represented.
Cite as

Theodoros Papamakarios. A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{papamakarios:LIPIcs.MFCS.2023.74,
  author =	{Papamakarios, Theodoros},
  title =	{{A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{74:1--74:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.74},
  URN =		{urn:nbn:de:0030-drops-186085},
  doi =		{10.4230/LIPIcs.MFCS.2023.74},
  annote =	{Keywords: Proof Complexity, Resolution, Cut-free LK}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.100
Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems

Authors: Theodoros Papamakarios and Alexander Razborov

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We identify two new big clusters of proof complexity measures equivalent up to polynomial and log n factors. The first cluster contains, among others, the logarithm of tree-like resolution size, regularized (that is, multiplied by the logarithm of proof length) clause and monomial space, and clause space, both ordinary and regularized, in regular and tree-like resolution. As a consequence, separating clause or monomial space from the (logarithm of) tree-like resolution size is the same as showing a strong trade-off between clause or monomial space and proof length, and is the same as showing a super-critical trade-off between clause space and depth. The second cluster contains width, Σ₂ space (a generalization of clause space to depth 2 Frege systems), both ordinary and regularized, as well as the logarithm of tree-like size in the system R(log). As an application of some of these simulations, we improve a known size-space trade-off for polynomial calculus with resolution. In terms of lower bounds, we show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4. We introduce on our way yet another proof complexity measure intermediate between depth and the logarithm of tree-like size that might be of independent interest.
Cite as

Theodoros Papamakarios and Alexander Razborov. Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 100:1-100:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{papamakarios_et_al:LIPIcs.ICALP.2022.100,
  author =	{Papamakarios, Theodoros and Razborov, Alexander},
  title =	{{Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{100:1--100:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.100},
  URN =		{urn:nbn:de:0030-drops-164419},
  doi =		{10.4230/LIPIcs.ICALP.2022.100},
  annote =	{Keywords: Proof Complexity, Resolution, Size-Space Trade-offs}
}
  • Refine by Author
  • 2 Papamakarios, Theodoros
  • 1 Razborov, Alexander

  • Refine by Classification
  • 2 Theory of computation → Proof complexity

  • Refine by Keyword
  • 2 Proof Complexity
  • 2 Resolution
  • 1 Cut-free LK
  • 1 Size-Space Trade-offs

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2022
  • 1 2023

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact