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

Anupam Das 1, *
* Auteur correspondant
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
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^O(log log n) -size monotone proofs of the weak pigeonhole principle with (1 + ε)n pigeons and n holes for ε = 1/ polylog n, thereby also improving the best known bounds for monotone proofs.
Type de document :
Communication dans un congrès
CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. Proceedings of CSL-LICS '14., pp.1 - 10, 2014, 〈10.1145/2603088.2603164〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01096154
Contributeur : Anupam Das <>
Soumis le : mardi 16 décembre 2014 - 20:48:50
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : lundi 23 mars 2015 - 14:36:31

Fichier

WeakMonProofsPHP-Extended.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Anupam Das. On the pigeonhole and related principles in deep inference and monotone systems. CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. Proceedings of CSL-LICS '14., pp.1 - 10, 2014, 〈10.1145/2603088.2603164〉. 〈hal-01096154〉

Partager

Métriques

Consultations de la notice

191

Téléchargements de fichiers

89