Stephen Cook, Antonina Kolokolova

We introduce a second-order system V_1-Horn of bounded arithmetic

formalizing polynomial-time reasoning, based on Graedel's

second-order Horn characterization of P. Our system has

comprehension over P predicates (defined by Graedel's second-order

Horn formulas), and only finitely many function symbols. Other

systems of polynomial-time reasoning either ...
more >>>