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 >>>

We consider a class, denoted APP, of real-valued functions
f:{0,1}^n\rightarrow [0,1] such that f can be approximated, to
within any epsilon>0, by a probabilistic Turing machine running in
time poly(n,1/epsilon). We argue that APP can be viewed as a
generalization of BPP, and show that APP contains a natural
complete ... more >>>