We formalize the proof of Reingold's Theorem that SL=L (STOC'05) in the theory of bounded arithmetic VL, which corresponds to ``logspace reasoning''. As a consequence, we get that VL=VSL, where VSL is the theory of bounded arithmetic for ``symmetric-logspace reasoning''. This resolves in the affirmative an old open question from ... more >>>

We prove an easy-witness lemma ($\ewl$) for unambiguous non-deterministic verfiers. We show that if $\utime(t)\subset\mathcal{C}$, then for every $L\in\utime(t)$, for every $\utime(t)$ verifier $V$ for $L$, and for every $x\in L$, there is a certificate $y$ satisfing $V(x,y)=1$, that can be encoded as a truth-table of a $\mathcal{C}$ circuit. Our ... more >>>