1 Search Results for "Baaz, Matthias"

Document
DOI: 10.4230/LIPIcs.CSL.2015.94
Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic

Authors: Matthias Baaz and Christian G. Fermüller

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.
Cite as

Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baaz_et_al:LIPIcs.CSL.2015.94,
  author =	{Baaz, Matthias and Ferm\"{u}ller, Christian G.},
  title =	{{Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{94--109},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.94},
  URN =		{urn:nbn:de:0030-drops-54097},
  doi =		{10.4230/LIPIcs.CSL.2015.94},
  annote =	{Keywords: Cut-elimination, sequent calculus, intuitionistic logic}
}
  • Refine by Author
  • 1 Baaz, Matthias
  • 1 Fermüller, Christian G.

  • Refine by Classification

  • Refine by Keyword
  • 1 Cut-elimination
  • 1 intuitionistic logic
  • 1 sequent calculus

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

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