Proof complexity of intuitionistic implicational formulas

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F17%3A00464411" target="_blank" >RIV/67985840:_____/17:00464411 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1016/j.apal.2016.09.003" target="_blank" >http://dx.doi.org/10.1016/j.apal.2016.09.003</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.apal.2016.09.003" target="_blank" >10.1016/j.apal.2016.09.003</a>

Result language
angličtina
Original language name
Proof complexity of intuitionistic implicational formulas
Original language description
We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubeš (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jeřábek (2009), can be realized by implicational tautologies.
Czech name
—
Czech description
—

Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics

Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2017
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)