Number of the records: 1

Proof Complexity of the Cut-free Calculus of Structures

SYSNO ASEP	0323402
Document Type	J - Journal Article
R&D Document Type	Journal Article
Subsidiary J	Článek ve WOS
Title	Proof Complexity of the Cut-free Calculus of Structures
Title	Důkazová složitost bezřezového kalkulu struktur
Author(s)	Jeřábek, Emil (MU-W)_{RID, SAI, ORCID}
Source Title	Journal of Logic and Computation - ISSN 0955-792X Roč. 19, č. 2 (2009), s. 323-339
Number of pages	17 s.
Language	eng - English
Country	GB - United Kingdom
Keywords	proof complexity ; calculus of structures ; monotone sequent calculus
Subject RIV	BA - General Mathematics
CEZ	AV0Z10190503 - MU-W (2005-2011)
UT WOS	000264656300006
Annotation	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.
Workplace	Mathematical Institute
Contact	Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757
Year of Publishing	2009

Number of the records: 1