If $F$ is valid then $F \cup res(C_1,C_2,A_i)$ is valid
I have to prove the following problem in propositional logic:
Let $F$ be a set of clauses and let $F' = F \cup {res(C_1,C_2,A_i)}$ be the extension of $F$ by a resolvent of some clauses $C_1,C_2 \in F$ where $A_i$ is a literal occuring positively in $C_1$ and negatively in $C_2$.
Prove that: If $F$ is valid, then $F'$ is valid.
So in other words I have to prove that when I construct the union of the original formula $F$ and the formula resulting by applying resolution on $F$ over a literal $A_i$ in $F$, validity is still preserved.
I think that this should be provable by applying a direct proof.
Recall: Note that resolution is defined as follows: given two clauses: $C_1 = (A_1 \lor \dots \lor A_i \lor \dots \lor A_n)$ and $C_2 = (B_1 \lor \dots \lor B_j \lor \dots \lor B_m)$ such that for some $i, j$ with $1 \leq i \leq n$, and $1 \leq j \leq m,\; A_i = \neg B_j$,
the resolvent of $C_1$ and $C_2$ on $A_i$ is the clause
$res(C_1,C_2,A_i) = (A_1 \lor \dots \lor A_{i-1} \lor A_{i+1} \lor \dots \lor A_n \lor B_1 \lor \dots B_{j-1} \lor B_{j+1} \lor \dots \lor B_m)$
EDIT: Here is my try:
Let $I$ be an interpratation taken from the set of models $Mod(F)$. Hence, $I(F) = 1$. Because this interpretation satisfies $F$ it must also be the case that it satisfies $C_1$ and $C_2$. 945
If we take a look at the structure of $C_1$ and $C_2$ we have to distinguish between $2$ different cases:
(1) $A_i$ is positive in $C_1$ but negative in $C_2$ and
(2) $A_i$ is negative in $C_1$ but positive in $C_2$.
In case (1) if $A_i$ is set to true in $C_1$ it would be false in $C_2$. In case (2) if $A_i$ is set to true in $C_2$ it would be false in $C_1$.
$A_i$ cannot be the literal which preserves satisfiability of $F$. Hence $I$ must include some assignment of other literals in $F$ such that $F$ is satisfied. Thus, the resolvant $res(C_1,C_2,A_i)$ is also satisfied. 610