Cut-Admissibility as a Corollary of the Subformula Property.
Lecture Notes in Artificial Intelligence(2017)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络