We identify two wide families of propositional sequent calculi for which cut-admissibility is a corollary of the subformula property. While the subformula property is often a simple consequence of cut-admissibility, our results shed light on the converse direction, and may be used to simplify cut-admissibility proofs in various propositional sequent calculi. In particular, the results of this paper may be used in conjunction with existing methods that establish the subformula property, to obtain that cut-admissibility holds as well.
CITATION STYLE
Lahav, O., & Zohar, Y. (2017). Cut-admissibility as a corollary of the subformula property. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10501 LNAI, pp. 65–80). Springer Verlag. https://doi.org/10.1007/978-3-319-66902-1_4
Mendeley helps you to discover research relevant for your work.