On the pigeonhole and related principles in deep inference and monotone systems

A. Das

Research output: Chapter in Book/Report/Conference proceedingChapter

6 Citations (Scopus)

Abstract

We construct quasipolynomial-size proofs of the propositional pigeonhole principle in the deep inference system KS, addressing an open problem raised in previous works and matching the best known upper bound for the more general class of monotone proofs. We make significant use of monotone formulae computing boolean threshold functions, an idea previously considered in works of Atserias et al. The main construction, monotone proofs witnessing the symmetry of such functions, involves an implementation of merge-sort in the design of proofs in order to tame the structural behaviour of atoms, and so the complexity of normalization. Proof transformations from previous work on atomic flows are then employed to yield appropriate KS proofs. As further results we show that our constructions can be applied to provide quasipolynomial-size KS proofs of the parity principle and the generalized pigeonhole principle. These bounds are inherited for the class of monotone proofs, and we are further able to construct n-size monotone proofs of the weak pigeonhole principle with (1 + ε)n pigeons and n holes for ε = 1= logk n, thereby also improving the best known bounds for monotone proofs.

Original languageEnglish
Title of host publicationProceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
PublisherAssociation for Computing Machinery
ISBN (Print)9781450328869
DOIs
Publication statusPublished - 2014
EventJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014 - Vienna , Austria
Duration: 14 Jul 201418 Jul 2014

Conference

ConferenceJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014
CountryAustria
CityVienna
Period14/07/1418/07/14

Fingerprint Dive into the research topics of 'On the pigeonhole and related principles in deep inference and monotone systems'. Together they form a unique fingerprint.

Cite this