Simulating non‐prenex cuts in quantified propositional calculus
Simulating non‐prenex cuts in quantified propositional calculus
复制标题
模拟量化命题演算中的非 prenex 削减
DOI：
--
复制
发表时间：
2011
影响因子：
0.3
通讯作者：
Phuong Nguyen
中科院分区：
文献类型：
--
作者：
Emil Jeřábek;Phuong Nguyen
我们证明了量化命题证明系统Gi是多项式等价于它们的限制版本，要求所有的切割公式是前向收缩的（或前向收缩的）。此前，这仅针对树状系统G*i而知。© 2011 WILEY‐VCH Verlag GmbH & Co. KGaA，魏因海姆
We show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex Σqi (or prenex Πqi). Previously this was known only for the treelike systems G*i. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim