-1
$\begingroup$

I'm trying to do the following demonstration:

(C and S are CNF) C is a logical consequence of S iff. S u {-C} UNSAT

And I did the following:

C is a logical consequence of S iff. S u {-C} UNSAT iff.

for all interpretation I that SAT S -> I SAT C iff.

for all I, eval_I(S) = 1 -> eval_I(C) = 1 iff.

for all I, -eval_I(S) = 1 or eval_I(C) = 1 iff.

for all I, eval_I(S) = 0 or eval_I(C) = 1 iff...

And I got stuck right there. Any clues? Thaks!

$\endgroup$
0
$\begingroup$

You need to apply De Morgan at some point. Trying to stick with your notation:

for all interpretations I, I SAT S -> I SAT C
iff
for all interpretations I, not(not(I SAT S -> I SAT C))
iff
for all interpretations I, not(I SAT S and not I SAT C)
iff
for all interpretations I, not(I SAT S and I SAT -C)
iff
not exists interpretation I, (I SAT S and I SAT -C)
iff
not exists interpretation I, I SAT (S u {-C})
iff
not SAT (S u {-C})
iff
UNSAT (S u {-C})
$\endgroup$

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.