Comparison of two ways of checking resolution refutations

[ceilican]

There are (at least) two possible ways of checking that a resolution refutation (with omitted intermediary resolvents and explicit pivots) is correct:

1. to traverse it top-down, computing all the intermediary resolvents and finally checking that the root resolvent is the empty clause.
2. to traverse it bottom-up, computing safe literals (as in RPI) for each node and, finally checking that each axiom clause is a subset of its corresponding safe literals.

Could the second way be more efficient than the first way?

Was this already investigated in the literature? Here are some pointers:

• http://user.it.uu.se/~tjawe125/talks/efficiently-checking-propositional-resolution-proofs-in-isabelle-hol.pdf
• http://ie.technion.ac.il/SMT09/slides/M3.pdf
• ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/StuEtAl-FMSD-12.pdf