Suppose you're given this KB:
$$KB = (A, A ⇒ B, A ⇒ C, B ∧ C ⇒ D)$$
How would you show using a SAT solver that $KB \vDash D$?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
TL;DR: Use the SAT solver to search for a counterexample.
To check that $KB \models \varphi$, you need to know whether there is any assignment that is consistent with $KB$ but that does not satisfy $\varphi$. In other words, you need to know whether $KB \land \neg \varphi$ is satisfiable or not. If $KB \land \neg \varphi$ is satisfiable, then you have found a counterexample that demonstrates that $KB \not\models \varphi$. If $KB \land \neg \varphi$ is not satisfiable, then you proven that $KB \models \varphi$ is true.
Now apply that to your specific example.
