Extension without cut

DOI10.1016/J.APAL.2012.07.004zbMATH Open1256.03018OpenAlexW2164449415MaRDI QIDQ714731FDOQ714731

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

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

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)

Cites Work

• Untersuchungen über das logische Schliessen. I
• Title not available (Why is that?)
• Title not available (Why is that?)
• The relative efficiency of propositional proof systems
• Towards an algorithmic construction of cut-elimination procedures
• On the proof complexity of deep inference
• Cirquent Calculus Deepened
• The intractability of resolution
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Polynomial size proofs of the propositional pigeonhole principle
• A Local System for Classical Logic
• Exploring the gap between linear and classical logic
• A system of interaction and structure
• On the axiomatisation of Boolean categories with and without medial
• MELL in the calculus of structures
• Bounds for proof-search and speed-up in the predicate calculus
• Towards a clausal analysis of cut-elimination
• Proof Transformation by CERES
• 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
• Proof Complexity of the Cut-free Calculus of Structures
• Title not available (Why is that?)

Cited In (10)

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

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)