Extension without cut

DOI10.1016/j.apal.2012.07.004zbMath1256.03018OpenAlexW2164449415MaRDI QIDQ714731

Lutz Straßburger

Publication date: 11 October 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2012.07.004

zbMATH Keywords

cut eliminationproof complexityFrege systemsbalanced tautologiesdeep inferencepropositional pigeonhole principle

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Classical propositional logic (03B05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items (8)

PROOF COMPLEXITIES ON A CLASS OF BALANCED FORMULAS IN SOME PROPOSITIONAL SYSTEMS ⋮ On the Power of Substitution in the Calculus of Structures ⋮ Enumerating Independent Linear Inferences ⋮ A System of Interaction and Structure III: The Complexity of BV and Pomset Logic ⋮ On linear rewriting systems for Boolean logic and some applications to proof theory ⋮ On the Proof Complexity of Cut-Free Bounded Deep Inference ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Unnamed Item

Uses Software

• CERES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Untersuchungen über das logische Schliessen. I
• MELL in the calculus of structures
• Towards a clausal analysis of cut-elimination
• On the proof complexity of deep inference
• A Local System for Classical Logic
• On the Proof Complexity of Cut-Free Bounded Deep Inference
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• From Deep Inference to Proof Nets via Cut Elimination
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Cirquent Calculus Deepened
• Proof Complexity of the Cut-free Calculus of Structures
• Polynomial size proofs of the propositional pigeonhole principle
• The relative efficiency of propositional proof systems
• Bounds for proof-search and speed-up in the predicate calculus
• A system of interaction and structure
• Towards an algorithmic construction of cut-elimination procedures
• Proof Transformation by CERES

This page was built for publication: Extension without cut