3
$\begingroup$

Consider the following statement

In FOL, we can reduce entailment checking to satisfiability checking:

$S \models S' \iff S \land \neg S'$ is satisfiable (This proof strategy is called refutation).

Is the above statement true? If yes, then I got confusion because of the following steps

$ S \models S' \iff S\implies S'$ is true

$S \models S' \iff \neg S \lor S'$ is satisfiable

$S \models S' \iff \neg( S \land \neg S') $ is satisfiable

$S \models S' \iff S \land \neg S' $ is unsatisfiable

Which one is true?

$\endgroup$
  • 1
    $\begingroup$ This is a math question, and belongs in Mathematics. $\endgroup$ – Yuval Filmus Feb 3 at 15:38
  • 2
    $\begingroup$ @YuvalFilmus I disagree. Logic is fundamental to CS. $\endgroup$ – David Richerby Feb 3 at 16:40
3
$\begingroup$

This looks like a typo in your source, and your derivation looks correct. So the corrected statement should be:

$S \models S' \iff S \land \neg S'$ is unsatisfiable

or

$S \models S' \iff {\boldsymbol \neg} (S \land \neg S')$ is satisfiable

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