Extension without cut
type: Item
instance of: scholarly article
title: Extension without cut
zbMATH Open document ID: 1256.03018
author: Lutz Straßburger
published in: Annals of Pure and Applied Logic
publication date: 2012-10-11T00:00:00Z
review text: The extension rule introduces a new propositional variable \(x\) denoting formula \(A\) by adding \(A\to x\) and \(x\to A\). The author claims that ``there is no such thing as a cut-free extended Frege system''. He defines cut-free extension systems for deep inference.
reviewed by: G. E. Mints
Mathematics Subject Classification ID: 03B05
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 6092975
zbMATH Keywords: deep inference
zbMATH Keywords: Frege systems
zbMATH Keywords: proof complexity
zbMATH Keywords: cut elimination
zbMATH Keywords: propositional pigeonhole principle
zbMATH Keywords: balanced tautologies
describes a project that uses: CERES
MaRDI profile type: Publication
full work available at URL: j.apal.2012.07.004
OpenAlex ID: W2164449415
cites work: Proof Transformation by CERES
cites work: Towards a clausal analysis of cut-elimination
cites work: A Local System for Classical Logic
cites work: On the proof complexity of deep inference
cites work: A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
cites work: Polynomial size proofs of the propositional pigeonhole principle
cites work: Towards an algorithmic construction of cut-elimination procedures
cites work: The relative efficiency of propositional proof systems
cites work: On the Proof Complexity of Cut-Free Bounded Deep Inference
cites work: Untersuchungen über das logische Schliessen. I
cites work: A system of interaction and structure
cites work: Q4783301
cites work: The intractability of resolution
cites work: Cirquent Calculus Deepened
cites work: Proof Complexity of the Cut-free Calculus of Structures
cites work: Propositional proof systems, the consistency of first order theories and the complexity of computations
cites work: Q5423981
cites work: Bounds for proof-search and speed-up in the predicate calculus
cites work: Q5423982
cites work: MELL in the calculus of structures
cites work: From Deep Inference to Proof Nets via Cut Elimination
cites work: Q4499084
cites work: Q5593816
DOI: 10.1016/J.APAL.2012.07.004
description: scientific article; zbMATH DE number 6092975