Refutation

Resolution by refutation to show $\text{KB}\models A$ Knowledge base

• Assume $\neg A$ is true to generate a contradiction (refutation).
• Convert $\neg A$ and all sentences in the KB to a clausal theory $C$.
• Resolve the clauses in $C$ until an empty clause is obtained.