0
$\begingroup$

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$. 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.

$\endgroup$
  • $\begingroup$ What kind of logic are you considering? Propositional or predicate? $\endgroup$ – babou Mar 27 '15 at 9:31
  • $\begingroup$ I am considering propositional logic. $\endgroup$ – user1291235 Mar 27 '15 at 9:33
  • $\begingroup$ Satisfiability must be verified for each of the clauses, which are disjunctions of literals. Hence there must be at least one literal in each clause that preserves satisfiability, though there may be several. Since $A_i=\neg B_j$, one of them must be satisfied by an interpretation, and can be the one that preserve satisfiability in the corresponding clause $C_1$ or $C_2$. In the one clause where it is not satisfied, there must be some other literal $A_k$ or $B_k$ that is satisfied, since the clause is satisfied by hypothesis. Since this literal is part of the resolvent, it is also satisfied. $\endgroup$ – babou Mar 29 '15 at 7:54
2
$\begingroup$

Since you are only asking for a hint:

You have to prove that, for any interpretation I, if it satisfies all the clauses in $F$, then it also satisfies the resolvant $res(C_1,C_2,A_i)$, and hence it satisfies all the clauses in $F'$.

From that you can infer the result to be proved, with some universal quantification.

Note on terminology and notations:

  • I would rather say that, when $F$ is valid, every interpretation satisfies it. It is $F$ that is to be satisfied, not the interpretation. Or more generally, it may also be a clause $C$, a literal $A_i$, or a set of clauses $F$ that may (have to) be satisfied.

  • $F$ is valid iff for any interpretation $I$, $I(F)=1$.
    You should not say "for any interpretation $I(F)$", since as you noted yourself, $I(F)$ is a truth value. An interpretation in propositional logic is (usually) an assignment of truth values to the symbols used in the clauses, i.e. a mapping of the set of symbols to the set of truth values. It also implies interpreting logical connectives in the usual way, and sets of clauses as a conjunction of the clauses. Then, truth tables allow you to associate truth values to each construct, up to the whole set of clauses, which is what is meant by $I(F)$. The interpretation is $I$. while $I(F)$ is the truth value it gives to the set $F$ of clauses.

Interpretation may be defined in a more general way, but the above should be enough here.

$\endgroup$
  • $\begingroup$ Ok. I take an interpretation $I$ from the set of models $Mod(F)$. Hence this interpretation makes the formula setisfiable,i.e., $I(F) = 1$. How can I argue that the resolvant is also satisfiable? May I argue that the literal ($A_i$) which is positive in one clause and negative in the other cannot be the literal which preserves validity? So if I delete it (with resolution) the formula is still satisfiable / valid? $\endgroup$ – user1291235 Mar 27 '15 at 14:07
  • $\begingroup$ @user1291235 You consider an interpretation $I$ that satisfies $F$. Hence it must also satisfy $C_1$ and $C_2$. Thus, since each $C_i$ is a disjunction, there must be in each a literal that is satisfied ... . Then you have some cases to consider, depending on what the literal may be for each. From that you conclude that the resolvant is also satified. Recall satisfied and satisfiable are not synonymous. Like this exercise: it is doable, but it is not done yet. $\endgroup$ – babou Mar 27 '15 at 14:40
  • $\begingroup$ Thank you for your advices, I've edited my question and included an first attempt of a proof. Is this going somewhat in the right direction? $\endgroup$ – user1291235 Mar 27 '15 at 15:17
  • $\begingroup$ It is sort of correct, but your way of stating it is much too loose and unclear. You should treat the two cases separately (though they are similar). If, for interpretation $I$, $I(A_i)=1$ and $I(B_j)=0$, then you know that, since $I(C_2)=1$, some other literal $B_k$ with $k\neq j$ in $C_2$ must be satisfied by $I$, i.e. $I(B_k)=1$ ... and what does it imply for the resolvant? You have to learn to write clear proofs and use precise language. $\endgroup$ – babou Mar 27 '15 at 15:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.