The Complexity of Gentzen Systems for Propositional Logic
The Complexity of Gentzen Systems for Propositional Logic
复制标题
命题逻辑 Gentzen 系统的复杂性
DOI：
10.1016/0304-3975(89)90147-3
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
A. Urquhart
中科院分区：
文献类型：
--
作者：
A. Urquhart
给出了经典命题逻辑中只涉及双条件且需要指数长证明的有效序列的例子。如果允许切割规则，则序列具有多项式大小证明。
Examples are given of valid sequents of classical propositional logic involving only the biconditional which require exponentially long proofs in a cut-free Gentzen system. The sequents have polynomial size proofs if the cut rule is allowed.