1
$\begingroup$

Resolution algorithm from AIMA pg 255

The standard resolution algorithm returns false if no new clauses are added.

I know that if $KB \land \neg a \implies []$, it returns true by proof by contradiction, but how can I understand the false case intuitively?

$\endgroup$
4
$\begingroup$

When $new\subseteq clauses$ then, if we continued, the next line would be $clauses \leftarrow clauses\cup new$ but $clauses\cup new = clauses$ so we'd be doing the exact same calculation the next time through the loop deducing nothing new and looping forever.

The point is, if we "resolve" all pairs of clauses and deduce nothing new, then we've derived all the consequences from the original set of clauses. If we still haven't derived a contradiction at that point, then $\neg\alpha$ is consistent with $KB$ and thus $\alpha$ is not provable. This last isn't necessarily completely accurate either, as it only shows that $\alpha$ is not a propositional consequence of $KB$. For example, if $KB$ was $\forall x.P(x)$ and $\alpha$ was $P(t)$, then $\alpha$ is provable from $KB$ but not via propositional reasoning.

$\endgroup$
  • $\begingroup$ $\neg \alpha$ is consistent with $KB$, also one may be able to extract a model that satisfies $KB$ and $\neg\alpha$ from the set $clauses$. Thus $\alpha$ is not provable under the assumptions contained in $KB$. However as I understand, at this point we cannot say that $\neg\alpha$ is true. $\endgroup$ – Dmitri Chubarov Apr 28 '18 at 14:49
  • $\begingroup$ @DmitriChubarov Yes, that is correct. $\endgroup$ – Derek Elkins Apr 28 '18 at 19:12

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.