On the Power of Substitution in the Calculus of Structures

DOI10.1145/2701424zbMath1354.03091OpenAlexW1979474827MaRDI QIDQ2946759

Novak Novaković, Lutz Straßburger

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2701424

zbMATH Keywords

extensionproof complexityclassical logicsubstitutionFrege systemsdeep inferencecalculus of structures

Mathematics Subject Classification ID

Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items (2)

The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• Extension without cut
• Cut elimination inside a deep inference system for classical predicate logic
• The undecidability of \(k\)-provability
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Untersuchungen über das logische Schliessen. I
• Complexity of Deep Inference via Atomic Flows
• On the proof complexity of deep inference
• A system of interaction and structure IV
• Rewriting with Linear Inferences in Propositional Logic
• A Local System for Classical Logic
• A system of interaction and structure V: the exponentials and splitting
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Normalisation Control in Deep Inference via Atomic Flows
• Proof Complexity of the Cut-free Calculus of Structures
• The relative efficiency of propositional proof systems
• Bounds for proof-search and speed-up in the predicate calculus
• Logic Programming
• A system of interaction and structure
• Computer Science Logic
• Subformula Linking as an Interaction Method
• Reducing Nondeterminism in the Calculus of Structures

This page was built for publication: On the Power of Substitution in the Calculus of Structures