Resolution algorithm

Let $\mathcal{P}$ be a definite clause program with rules ${}^{\prime }{B}_1,\dots ,B_m\to H^{\prime }$, where $m\ge 0$, and let ${}^{\prime }?Q_1,...,Q_n^{\prime }$ be a conjunctive query over $\mathcal{P}$.

1. Set progress to $\top$.
2. Set currentGoal to $?Q_1,...,Q_n$.
3. While the currentGoal is not empty and progress is $\top$:
   1. Let $\bar{Q}=Q_i$ be a proposition in the current goal.
   2. If it exists, choose in $\mathcal{P}$ a rule with the head $\bar{Q}$.
      1. Let $B_1,\dots ,B_m\to \bar{Q}$ be a rule in $\mathcal{P}$ with the head $\bar{Q}$.
      2. In the current goal, replace $\bar{Q}=Q_i$ for $B_1,\dots ,B_m$: $?(Q_1,\dots ,Q_{i-1}),(B_1,\dots ,B_m),(Q_{i+1},\dots ,Q_n)$
   3. Else, set progress to $\perp$.
4. If currentGoal is empty and progress is $\top$ then the output is true, otherwise the output is false.

There are two points of non-determinism:

• (3.1) When we choose a proposition in the current goal. The choice here does not matter but we must be consistent, i.e. always leftmost or rightmost.
• (3.2) When we choose a matching rule, this choice does matter. See example 2 for an explanation.