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
- ¬ a or ¬ b
- (a or b) and (a or c)
- (b or d) and (¬ c or d)
- ¬ d or e
- ¬ d (negation of goal)
We're trying to prove d.
How, do you handle those ANDs?
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$