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

Please wait, while we are loading the content...

Trade-off analysis meets probabilistic model checking

Understanding biology through logic

The Ackermann award 2014

Infinite-state energy games

Abstract interpretation: past, present and future

Computer-checked mathematics: a formal proof of the odd order theorem

Citations for the test-of-time award from 1994

Beta reduction is invariant, indeed

Regular combinators for string transformations

Asymptotic behaviour in temporal logic

Weight monitoring with linear temporal logic: complexity and decidability

Graph logics with rational relations: the role of word combinatorics

Effective interpolation and preservation in guarded logics

On the discriminating power of passivation and higher-order interaction

A domain-theoretic approach to Brownian motion and general continuous stochastic processes

Two-way cost automata and cost logics over infinite trees

Decomposition theorems and model-checking for the modal μ-calculus

Logic for communicating automata with parameterized topology

Logical characterization of weighted pebble walking automata

Coinduction up-to in a fibrational setting

Model checking existential logic on partially ordered sets

Zero-reachability in probabilistic multi-counter automata

The complexity of admissibility in Omega-regular games

On the characterization of models of H

A decision procedure for satisfiability in separation logic with inductive predicates

Secure equilibria in weighted games

Weak MSO: automata and expressiveness modulo bisimilarity

Symmetry in concurrent games

Decidability of weak logics with deterministic transitive closure

Equality and fixpoints in the calculus of structures

The tractability frontier of graph-like first-order query sets

One hierarchy spawns another: graph deconstructions and the complexity classification of conjunctive queries

On the total variation distance of labelled Markov chains

System F with coercion constraints

The geometry of synchronization

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

Expressive completeness of separation logic with two variables and no separating conjunction

A new correctness criterion for MLL proof nets

On periodically iterated morphisms

Pattern logics and auxiliary relations

Substitution, jumps, and algebraic effects

Satisfiability modulo counting: a new approach for analyzing privacy properties

Achieving new upper bounds for the hypergraph duality problem through logic

Symmetric normalisation for intuitionistic logic

Equilibria of concurrent games on event structures

Subclasses of presburger arithmetic and the weak EXP hierarchy

Senescent ground tree rewrite systems

Preservation and decomposition theorems for bounded degree structures

No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete

Abstract interpretation from Büchi automata

Memoryful geometry of interaction: from coalgebraic components to algebraic effects

Axioms and decidability for type isomorphism in the presence of sums

Functional reactive types

Probably safe or live

A quest for algorithmically random infinite structures

On the succinctness of query rewriting over shallow ontologies

Turing machines with atoms, constraint satisfaction problems, and descriptive complexity

Local temporal reasoning

On Hanf-equivalence and the number of embeddings of small induced subgraphs

Non-elementary complexities for branching VASS, MELL, and extensions

Infinite sequential games with real-valued payoffs

Hyper-Ackermannian bounds for pushdown vector addition systems

Transition systems over games

Compositional verification of termination-preserving refinement of concurrent programs

Eilenberg-MacLane spaces in homotopy type theory

MSO queries on trees: enumerating answers under updates

On the computing power of +, -, and ×

On the Hoare theory of monadic recursion schemes

Formulae-as-types for an involutive negation

A type theory for productive coprogramming via guarded recursion

Deadlock and lock freedom in the linear π-calculus

On context semantics and interaction nets

Anchored LTL separation

Separating regular languages with first-order logic

Logics with counting and equivalence

A functional functional interpretation

Compositional higher-order model checking via ω-regular games over Böhm trees

Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives

Faster decision of first-order graph properties

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

Content Provider	ACM Digital Library
Author	Das, Anupam
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 nO(log log n)-size monotone proofs of the weak pigeonhole principle with (1 + ε)n pigeons and n holes for ε = $1/log^{k}$ n, thereby also improving the best known bounds for monotone proofs.
Starting Page	1
Ending Page	10
Page Count	10
File Format	PDF
ISBN	9781450328869
DOI	10.1145/2603088.2603164
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-07-14
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Atomic flows Pigeonhole principle Deep inference Monotone proofs
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in