I've seen multiple examples of how resolution works when one has two disjunctive clauses with one having a negated literal present in the other clause. And when you resolve the two, you eliminate the complimentary literals and end up with a disjunction of the remaining clauses. An example on Wikipedia shows this:

$$\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }$$

However, what does one do when your clauses don't just contain OR'd clauses? Like let's say you have a KB like so

  1. ¬ a or ¬ b
  2. (a or b) and (a or c)
  3. (b or d) and (¬ c or d)
  4. ¬ d or e
  5. ¬ d (negation of goal)

We're trying to prove d.

How, do you handle those ANDs?


1 Answer 1


You simply remove the and’s, thus obtaining separate disjunctive clauses.

For example, $(a \lor b) \land (a \lor c)$ simply becomes two separate clauses $a \lor b $ and $ a \lor c$


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .