Extension without cut

DOI10.1016/J.APAL.2012.07.004MaRDI QIDQ714731zbMATHOpenAlexFDO

Authors 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

proof complexitycut eliminationFrege systemsbalanced tautologiesdeep inferencepropositional pigeonhole principle

Mathematics Subject Classification ID

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

Recommendations

• From deep inference to proof nets via cut elimination
• Cut rule for the resolution method
• Substitution Frege and extended Frege proof systems in non-classical logics
• scientific article; zbMATH DE number 806751
• Frege systems for extensible modal logics

Cites work

• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 1841813 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• A Local System for Classical Logic
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• A system of interaction and structure
• Bounds for proof-search and speed-up in the predicate calculus
• Cirquent Calculus Deepened
• Exploring the gap between linear and classical logic
• From deep inference to proof nets via cut elimination
• MELL in the calculus of structures
• On the axiomatisation of Boolean categories with and without medial
• On the proof complexity of cut-free bounded deep inference
• On the proof complexity of deep inference
• Polynomial size proofs of the propositional pigeonhole principle
• Proof Complexity of the Cut-free Calculus of Structures
• Proof Transformation by CERES
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• The intractability of resolution
• The relative efficiency of propositional proof systems
• Towards a clausal analysis of cut-elimination
• Towards an algorithmic construction of cut-elimination procedures
• Untersuchungen über das logische Schliessen. I

Cited in

(11)

• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• On linear rewriting systems for Boolean logic and some applications to proof theory
• PROOF COMPLEXITIES ON A CLASS OF BALANCED FORMULAS IN SOME PROPOSITIONAL SYSTEMS
• Enumerating Independent Linear Inferences
• On the Power of Substitution in the Calculus of Structures
• Uniqueness of axiomatic extensions of cut-free classical propositional logic
• On the proof complexity of cut-free bounded deep inference
• scientific article; zbMATH DE number 7204450 (Why is no real title available?)
• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• Proof Complexity of the Cut-free Calculus of Structures
• Extended cuts

Describes a project that uses

Uses Software

• CERES

This page was built for publication: Extension without cut

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q714731)