Resolution vs Nondeterministic Search Problems
If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/howtolie.ps). The queries are formulas (not just variables). The tree is also completely deterministic. 

Other decision trees that correspond to different propositional proof systems exist: e.g., Linear Decision Trees correspond to Res(lin) refutations (cf., http://www.csc.kth.se/~sokolovd/files/papers/splitting.pdf and http://cs.rhul.ac.uk/home/tzameret/Res-Lin-Two.pdf). But there are many other examples (cf., Tonian Pitassi's work on CP-like proof systems).