I have to prove the following problem in propositional logic: Let F be a set of
ID: 647068 • Letter: I
Question
I have to prove the following problem in propositional logic:
Let F be a set of clauses and let F?=F?{res(C1,C2,Ai)} be the extension of F by a resolvent of some clauses C1,C2?F where Ai is a literal occuring positively in C1 and negatively in C2.
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 Ai 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: C1=(A1???Ai???An) and C2=(B1???Bj???Bm) such that for some i,j with 1?i?n, and 1?j?m,Ai=
Explanation / Answer
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(C1,C2,Ai), 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 Ai, 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.