A deductive system in mathematical logic consists of rules of inference. A rule of inference states how to derive a new formula from some formulas that we have already.
A proof in a deductive system is a finite sequence of formulas where each formula is either a given formula, or derived from the earlier formulas in the sequence using a rule of inference in the system. The last element of the sequence is the conclusion of the proof.
For example, given S = {$p \to (q \to r)$, $p$, $q$} in a deductive system with one rule of inference which is Modus Ponens, we can prove $r$ by building a proof sequence:
The clause set in the algorithm functions like a proof sequence, but it is optimized to be space efficient.
To have a meaningful deductive system, we want all of rules of inference in the system to be sound. An example of an unsound rule is, "for a formula $A \lor B$, you can derive $A \land B$." This is obviously bad because, suppose you have "a banana is yellow or a banana is not yellow" (which is true), you should not be able to conclude that "a banana is yellow and a banana is not yellow" (which is false). An example of a sound rule is Modus Ponens. This is demonstrated in the assignment above.
Notice that both $r$ and $q \to p$ are consequences of S. While we see that we can derive $r$ in the above deductive system, it is impossible to derive $q \to p$ (you can try!). This is because our deductive system is very weak (it only has Modus Ponens), so it cannot prove everything that is true. There are some deductive systems which are complete, meaning they are capable of proving everything that is true.
Note: strictly speaking, a deductive system consists of something called axioms as well, but we will pretend for the sake of simplicity that axioms are a kind of rules of inference.
Our deductive system in the assignment which has only resolution rule is not complete either (can you construct a true formula which is not provable in the system?). In the algorithm, we claim that if we can't derive false, then we will conclude that it is satisfiable. This is a bold claim because if our system is just too weak to derive false while it is in fact possible to derive false in a stronger sound system, then we would have a wrong conclusion. However, our deductive system is, as we claim in the assignment, refutation-complete, meaning it is able to derive false from any unsatisfiable clause set.
Introduce two new symbols: ⊤ which is always evaluated to true, and ⊥ which is always evaluated to false (⊥ is exactly "false"). Let $subst(F, a, b)$ means a formula obtained from replacing all occurrences of $a$ with $b$ in $F$, and $remove(F, a)$ means a formula obtained from removing all occurrences of $a$ in $F$.
Consider a formula $F$. Let $p$ be a variable in $F$. Consider any truth assignment, either $p$ is assigned true or $p$ is assigned false. If $p$ is assigned true, the truth value of the formula would be $subst(F, p, \top)$. On the other hand, if $p$ is assigned false, the truth value of the formula would be $subst(F, p, \bot)$. So, intuitively, the formula $subst(F, p, \top) \lor subst(F, p, \bot)$ is satisfiable if and only if the original formula $F$ is satisfiable. Note that the formula $subst(F, p, \top) \lor subst(F, p, \bot)$ is known as a resolution of $F$ on $p$ (it's a different kind of resolution, but related).
As we limit our attention to $F$ which is in CNF form, divide $F$ into two groups: $A$ are clauses that do not contain variable $p$, $B$ are clauses that contain positive literal $p$, $C$ are clauses that contain negative literal $\neg p$. If a clause contains both $p$ and $\neg p$, choose to put it in one of $B$ or $C$ arbitrarily.
What will happen with $subst(F, p, \top)$ as we try to simplify it? $A$ won't be affected since there is no $p$. $B$ will become a clause of all tautologies (as a disjunction of ⊤ and anything is ⊤ which is a tautology itself). All occurences of $\neg p$ will basically get removed in $C$ as $\neg \top \lor \phi \equiv \bot \lor \phi \equiv \phi$ for any $\phi$.
What will happen with $subst(F, p, \bot)$ as we try to simplify it? $A$ won't be affected since there is no $p$. $C$ will become a clause of all tautologies (as a disjunction of ⊤ and anything is ⊤ which is a tautology itself). All occurences of $p$ will basically get removed in $B$ as $\bot \lor \phi \equiv \phi$ for any $\phi$.
So $F$ is satisfiable if and only if $(A \land remove(C, -p)) \lor (A \land remove(B, p))$ is satisfiable. By distribution law, the formula becomes $A \land (A \lor remove(B, p)) \land (A \lor remove(C, p) \land (remove(B, p) \lor remove(C, p))$. Note that $A$ implies $A \lor remove(B, p)$, so $A \lor remove(B, p)$ is weaker than $A$ and we can remove it safely without changing the satisfiability. The same argument applies to $A \lor remove(C, -p)$. This leads to a formula $A \land (remove(B, p) \lor remove(C, -p))$.
The punchline is that by distribution law, $remove(B, p) \lor remove(C, -p)$ are exactly all resolvents added to an iteration to eliminate $p$ in the algorithm, and $A \land (remove(B, p) \lor remove(C, -p))$ are exactly all clauses after an iteration to eliminate $p$!
By performing resolution of $F$ on every variable, we will definitely obtain whether or not $F$ is unsatisfiable. As the resolution rule corresponds to this action, the deductive system is refutation-complete as claimed.