On the proof complexity of deep inference
From MaRDI portal
Publication:2946572
DOI10.1145/1462179.1462186zbMATH Open1351.03056arXiv0709.1201OpenAlexW3123028025MaRDI QIDQ2946572FDOQ2946572
Authors: Paola Bruscoli, Alessio Guglielmi 
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Abstract: We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.
Full work available at URL: https://arxiv.org/abs/0709.1201
Recommendations
- On the proof complexity of cut-free bounded deep inference
- On the relative proof complexity of deep inference via atomic flows
- A formal proof of the expressiveness of deep learning
- A formal proof of the expressiveness of deep learning
- Deep network guided proof search
- True concurrency of deep inference proofs
- Deep inference and symmetry in classical proofs
- Provable approximation properties for deep neural networks
- From deep inference to proof nets via cut elimination
- Complexity of Deep Inference via Atomic Flows
Cited In (25)
- Extension without cut
- Complexity of Deep Inference via Atomic Flows
- On the logical philosophy of assertive graphs
- Contextual Natural Deduction
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Proof analysis of Peirce's alpha system of graphs
- A cirquent calculus system with clustering and ranking
- Maude as a platform for designing and implementing deep inference systems
- True concurrency of deep inference proofs
- On the Power of Substitution in the Calculus of Structures
- Implementation and evaluation of contextual natural deduction for minimal logic
- On the proof complexity of cut-free bounded deep inference
- From deep inference to proof nets via cut elimination
- A logical basis for quantum evolution and entanglement
- An Algorithmic Interpretation of a Deep Inference System
- On the relative proof complexity of deep inference via atomic flows
- Interaction and depth against nondeterminism in proof search
- Title not available (Why is that?)
- On the length of medial-switch-mix derivations
- A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
- A Subatomic Proof System for Decision Trees
- A propositional cirquent calculus for computability logic.
- Proof Complexity of the Cut-free Calculus of Structures
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- An Analytic Propositional Proof System on Graphs
This page was built for publication: On the proof complexity of deep inference
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946572)
