On the proof complexity of deep inference
From MaRDI portal
Publication:2946572
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.
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)- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Extension without cut
- Implementation and evaluation of contextual natural deduction for minimal logic
- An Analytic Propositional Proof System on Graphs
- On the length of medial-switch-mix derivations
- Complexity of Deep Inference via Atomic Flows
- An Algorithmic Interpretation of a Deep Inference System
- Interaction and depth against nondeterminism in proof search
- A logical basis for quantum evolution and entanglement
- On the logical philosophy of assertive graphs
- On the Power of Substitution in the Calculus of Structures
- A Subatomic Proof System for Decision Trees
- On the relative proof complexity of deep inference via atomic flows
- On the proof complexity of cut-free bounded deep inference
- From deep inference to proof nets via cut elimination
- A cirquent calculus system with clustering and ranking
- scientific article; zbMATH DE number 7204450 (Why is no real title available?)
- Contextual Natural Deduction
- Maude as a platform for designing and implementing deep inference systems
- Proof Complexity of the Cut-free Calculus of Structures
- Proof analysis of Peirce's alpha system of graphs
- True concurrency of deep inference proofs
- A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
- A propositional cirquent calculus for computability logic.
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)
