Počet záznamů: 1

Proof Complexity of the Cut-free Calculus of Structures

  1. 1.
    0323402 - MU-W 2009 RIV GB eng J - Článek v odborném periodiku
    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
    Výzkumný záměr: CEZ:AV0Z10190503
    Klíčová slova: proof complexity * calculus of structures * monotone sequent calculus
    Kód oboru RIV: BA - Obecná matematika
    Impakt faktor: 0.789, rok: 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.
    Trvalý link: http://hdl.handle.net/11104/0171376