On the relative proof complexity of deep inference via atomic flows

DOI10.2168/LMCS-11(1:4)2015MaRDI QIDQ5177335zbMATH OpenFDO

Authors Anupam Das

Publication date 11 March 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1502.05860

zbMATH Keywords

atomic flowsdeep inferencegraph rewritingnormalisationproof complexityproof theorypropositional logic

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Abstract: 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.

Recommendations

• Complexity of Deep Inference via Atomic Flows
• On the proof complexity of deep inference
• On the pigeonhole and related principles in deep inference and monotone systems
• Proof Complexity of the Cut-free Calculus of Structures
• Interaction and depth against nondeterminism in proof search

Cited in

(9)

• Complexity of Deep Inference via Atomic Flows
• On the proof complexity of deep inference
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• Normalisation Control in Deep Inference via Atomic Flows
• Proof Complexity of the Cut-free Calculus of Structures
• On the pigeonhole and related principles in deep inference and monotone systems
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• Enumerating Independent Linear Inferences
• Deep inference in proof search: the need for shallow inference

This page was built for publication: On the relative proof complexity of deep inference via atomic flows

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5177335)