Proof Complexity of the Cut-free Calculus of Structures

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F09%3A00323402" target="_blank" >RIV/67985840:_____/09:00323402 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Proof Complexity of the Cut-free Calculus of Structures
Original language description
We investigate the proof complexity of analytic subsystems of the deep inference proof system SKSg (the calculus of structures). Exploiting the fact that the cut rule (i {uparrow} )of SKSg corresponds to the left rule in the sequent calculus, we establish that the "analytic" system KSg + c{uparrow} has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSg + c{uparrow} quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonholeprinciple.
Czech name
Důkazová složitost bezřezového kalkulu struktur
Czech description
Zkoumáme důkazovou složitost analytických systémů důkazového systému hluboké inference SKSg (kalkulus struktur). S využitím faktu, že pravidlo řezu (i {uparrow} ) v SKSg odpovídá zavedení negace vlevo v sekventovém kalkulu, ukážeme, že "analytický" systém KSg + c{uparrow} ; má v podstatě stejnou složitost jako monotónní Gentzenův kalkulus MLK. Speciálně, KSg + c{uparrow} ; kvazipolynomiálně simuluje SKSg a dovoluje polynomiální důkazy některých variant principu PHP.

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
BA - General mathematics
OECD FORD branch
—

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

Similar results(10)