Das, Anupam - 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
On the relative proof complexity of deep inference via atomic flows

Authors: Das, Anupam

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.


Source : oai:arXiv.org:1502.05860
DOI : 10.2168/LMCS-11(1:4)2015
Volume: Volume 11, Issue 1
Published on: March 6, 2015
Submitted on: November 1, 2012
Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic


Share

Consultation statistics

This page has been seen 82 times.
This article's PDF has been downloaded 313 times.