2026-07-23T07:14:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5409 2024-03-06T10:36:24Z ddc:004 open_access

Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic Baaz, Matthias Fermüller, Christian G. Cut-elimination sequent calculus intuitionistic logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matthias Baaz and Christian G. Fermüller 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.94 urn:nbn:de:0030-drops-54097 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.94 eng https://creativecommons.org/licenses/by/3.0/legalcode