CORRECTIONS AND COMMENTS: 

Definition 2 on page 4:

"... iff |D| \subseteq |D'|." should read "... iff D \subseteq D'."

Definition 7 on page 7:

The selection of the pivot literals "v" and "\neg v" for producing the
resolvent is unprecise. For resolution on clauses (cubes), "v" must be
an existentially (universally) quantified variable.

See also slide 42 of our related talk:
http://fmv.jku.at/lonsing/talks/Lonsing-SAT10-talk.pdf

Definition 8 on page 7:

The definition "a := max({dl(l) | l \in R and dl(l) < d})" is too
coarse and can be refined. In fact, a more refined version has been
implemented in DepQBF 0.1 prior to writing this paper. See also source
code of function "get_reason_asserting_level".

See also slide 43 of our related talk:
http://fmv.jku.at/lonsing/talks/Lonsing-SAT10-talk.pdf