Proof complexity of intuitionistic implicational formulas

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Proof complexity of intuitionistic implicational formulas

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Proof complexity of intuitionistic implicational formulas

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2017

Kód důvěrnosti údajů

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

Název periodika

Annals of Pure and Applied Logic

ISSN

0168-0072

e-ISSN

—

Svazek periodika

168

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

41

Strana od-do

150-190

Kód UT WoS článku

000387529200008

EID výsledku v databázi Scopus

2-s2.0-84994908939