In the question, Translating SAT to HornSAT, Martin Seymour gives a method due to Joshua Grochow. It transforms 2-SAT into Horn-SAT, by creating a variable for every possible 2-SAT clause. Then, if a clause (or new variable) follows from two other clauses (variables) from "a single resolution step", it adds this implication to the formula. Finally, the unit clauses are added, along with a clause signifying not empty.
Can someone please explain, in detail, why we add clauses from "single resolution steps"? Am I correct in assuming that this means a single resolution step from unit propagation? Also, and perhaps most importantly, can someone prove that this method works?
Essentially, I'd like to know everything I can to ensure that I can implement this method, and also prove that it works. I'm also wondering if perhaps this method can be found in the literature somewhere.