Abstract | ||
---|---|---|
Abstract: We introduce a second-order system V1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Grädel's [15] second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Grädel's second-order Horn formulas), and only finitely many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates (such as Buss's S12 or the second-order V11), and hence are more powerful than our system (assuming the polynomial hierarchy does not collapse), or use Cobham's theorem to introduce function symbols for all polynomial-time functions (such as Cook's PV and Zambella's P-def). We prove that our system is equivalent to QPV and Zambella's P-def. Using our techniques, we also show that V1-Horn is finitely axiomatizable, and, as a corollary, that the class of \forall\Sigma_1^b consequences of S12 is finitely axiomatizable as well, thus answering an open question. |
Year | DOI | Venue |
---|---|---|
2001 | 10.1109/LICS.2001.932495 | Logic in Computer Science |
Keywords | Field | DocType |
np predicate,second-order system,second-order horn characterization,polytime reasoning,polynomial-time function,p predicate,second-order horn formula,function symbol,finitely axiomatizable,second-order v11,polynomial-time reasoning,computational complexity,second order system,polynomials,arithmetic,horn clauses,polynomial time,second order | Polynomial hierarchy,Discrete mathematics,Combinatorics,Horn clause,Bounded arithmetic,Second-order logic,Sigma,Predicate (grammar),Corollary,Mathematics,Computational complexity theory | Conference |
ISSN | ISBN | Citations |
1043-6871 | 0-7695-1281-X | 3 |
PageRank | References | Authors |
0.40 | 8 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Stephen Cook | 1 | 4864 | 2433.99 |
Antonina Kolokolova | 2 | 50 | 10.09 |