Quantified propositional calculus and a second-order theory for NC1

被引：0

作者：

Stephen Cook

Tsuyoshi Morioka

机构：

[1] University of Toronto,Department of Computer Science

[2] ,Hitachi Systems Development Laboratory

来源：

Archive for Mathematical Logic | 2005年 / 44卷

关键词：

Bounded Arithmetic; Computational Complexity; Proof Complexity;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively.

引用

页码：711 / 749

页数：38

共 15 条

[1]

Arai undefined(2000)undefined Ann. Pure Appl. Logic 103 155-undefined

[2]

Barrington undefined(1990)undefined J. Comput. Syst. Sci. 41 274-undefined

[3]

Buss undefined(1991)undefined Ann. Pure Appl. Logic 52 3-undefined

[4]

Buss undefined(1996)undefined Arch. Math. Logic 35 33-undefined

[5]

Buss undefined(3)undefined The Proceedings of the London Mathematical Society 60 1-undefined

[6]

Chiari undefined(1998)undefined The J. Symbolic Logic 63 1095-undefined

[7]

Clote undefined(1990)undefined A. Cook. Ann. Math. Art. Intell. 6 57-undefined

[8]

Cook undefined(2003)undefined Ann. Pure Appl. Logic 124 193-undefined

[9]

Cook undefined(1)undefined J. Symbolic Logic 44 36-undefined

[10]

Johnson undefined(1988)undefined Comput. Syst. Sci. 37 79-undefined

← 1 2 →