About Closure under Resolution

Question

The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. Thank you for your attention.

A CNF formula is closed under resolution if all the possible resolvents are subsumed by a clause of the formula - a clause $c_1$ is subsumed by a clause $c_2$ if all the literals of $c_2$ are in $c_1$ (any clause is subsumed by itself then).

Given $F$, a 3-CNF formula on $n$ variables $(x_i)$$_{i\le 1 \le n}$ which is closed under resolution. Given $I$, a partial assignment of $k$ variables among $(x_i)\ (k\le n)$. Let $F_{|I}$ the induced formula by applying $I$ to $F$: Any clause that contains a literal which evaluates to "true" under $I$ is deleted from the formula and any literals that evaluate to "false" under $I$ are deleted from all clauses - the clauses that become empty by this deletion remain in the formula as the empty clause.

Question: Is $F_{|I}$ closed under resolution ?

Answer 1

Sure. If $C_1\ni x_i$ and $C_2\ni\neg x_i$ are in $F\restriction I$ (in particular, $x_i$ is unset by $I$), pick clauses $D_1,D_2$ in $F$ which restrict to $C_1$ and $C_2$, respectively. Then $x_i\in D_1$ and $\neg x_i\in D_2$, hence their resolvent $(D_1\let\bez\smallsetminus\bez\{x_i\})\cup(D_2\bez\{\neg x_i\})$ is subsumed by some $D\in F$. If $D$ contains a literal made true under $I$, then so does $D_1$ or $D_2$, contradicting their choice. Thus, $D\restriction I$ is in $F\restriction I$, and it subsumes $(C_1\bez\{x_i\})\cup(C_2\cup\{\neg x_i\})$.