I have now learned resolution-based refutations in a lecture as well as from a book.

I have learned resolution of disjunctive normal form propositional logic to prove a formula inconsistent. This is a method of arguing by counter example the truth of a statement. We have just now covered the proofs for the soundness of this one step in this method namely the resolution rule of canceling a proposition and its negation, and then the soundness of the over all method, the refutation method and then the proof of the completeness of the method.