Anupam Das - On the relative proof complexity of deep inference via atomic flows

lmcs:735 - Logical Methods in Computer Science, March 6, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:4)2015
On the relative proof complexity of deep inference via atomic flowsArticle

Authors: Anupam Das ORCID

    We consider the proof complexity of the minimal complete fragment, KS, of standard deep inference systems for propositional logic. To examine the size of proofs we employ atomic flows, diagrams that trace structural changes through a proof but ignore logical information. As results we obtain a polynomial simulation of versions of Resolution, along with some extensions. We also show that these systems, as well as bounded-depth Frege systems, cannot polynomially simulate KS, by giving polynomial-size proofs of certain variants of the propositional pigeonhole principle in KS.

    https://doi.org/10.2168/LMCS-11(1:4)2015
    Source: arXiv.org:1502.05860
    Volume: Volume 11, Issue 1
    Published on: March 6, 2015
    Imported on: November 1, 2012
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic
    Licence: arXiv.org - Non-exclusive license to distribute

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    2 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 1601 times.
    This article's PDF has been downloaded 779 times.