Number of the records: 1
Proof Complexity of the Cut-free Calculus of Structures
- 1.0323402 - MÚ 2009 RIV GB eng J - Journal Article
Jeřábek, Emil
Proof Complexity of the Cut-free Calculus of Structures.
[Důkazová složitost bezřezového kalkulu struktur.]
Journal of Logic and Computation. Roč. 19, č. 2 (2009), s. 323-339. ISSN 0955-792X. E-ISSN 1465-363X
Institutional research plan: CEZ:AV0Z10190503
Keywords : proof complexity * calculus of structures * monotone sequent calculus
Subject RIV: BA - General Mathematics
Impact factor: 0.789, year: 2009
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 pigeonhole principle.
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.
Permanent Link: http://hdl.handle.net/11104/0171376
Number of the records: 1