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?
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.