Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
DOI10.1515/9781501502620-016zbMATH Open1433.03135OpenAlexW2500553567MaRDI QIDQ5221860FDOQ5221860
Authors: Sara Negri, Jan von Plato 
Publication date: 3 April 2020
Published in: Concepts of Proof in Mathematics, Philosophy, and Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1515/9781501502620-016
Recommendations
History of mathematics in the 20th century (01A60) Cut-elimination and normal-form theorems (03F05) History of mathematical logic and foundations (03-03) Structure of proofs (03F07)
Cited In (13)
- From cut-free calculi to automated deduction: the case of bounded contraction
- Title not available (Why is that?)
- Explaining the Gentzen-Takeuti reduction steps: A second-order system
- The Jacobson radical for an inconsistency predicate
- THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
- On permuting cut with contraction
- Reading conclusions conjunctively
- The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
- On Gentzen's structural completeness proof
- Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut
- A sequent calculus with implicit term representation
- Gentzen's consistency proof without heightlines
- A proof of Gentzen's \textit{Hauptsatz} without multicut
This page was built for publication: Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5221860)
