# Prolog resolution

Suppose we have the following knowledge base:

```f(a).
f(b).

g(a).
g(b).

h(b).

k(X) :- f(X), g(X), h(X).
```

How does Prolog determine whether `k(Y)` is true (provable)? That is, how does Prolog determine the value for `Y` that makes the query true?

Its search process can be see in this graphic. The process is as follows:

1. Create a temporary variable `_G34` (randomly-named) to stand in for `Y`. This is an implementation detail, so that if some other rule uses `Y` (a completely different variable), then the variable names don't collide.
2. The goal is to prove `k(_G34)`. To do so, proving ```f(_G34), g(_G34), h(_G34)``` will be enough. This is the new goal.
3. To satisfy the first part of the new goal, `f(_G34)`, the knowledge base is searched. There is no rule for `f/1` (the predicate with arity one) but there is a fact: `f(a)`. The first matching fact/rule is tried first. Thus, `_G34` gets set to `a` (from unification).
4. Now, `g(a), h(a)` is the new goal. `g(a)` is satisfied just fine, because exactly that term is found in the knowledge base (trivial unification).
5. Now, `h(a)` is the new goal. But, nothing in the knowledge base unifies with `h(a)` and there is no `h/1` rule, so there is a problem.
6. Go to the last decision point. This was when `_G34` was set to `a`. Try to set it to something else. `f(b)` is in the knowledge base as well, so go with `_G34 = b`.
7. The new goal is `g(b), h(b)`, etc… (which ultimately works). Now we'll switch to this knowledge base:

```loves(vincent, mia).
loves(marcellus, mia).
jealous(A, B) :- loves(A, C), loves(B, C).
```

How does Prolog find the proof for `jealous(X, Y)`, and what values do the variables take?

The proof tree is shown below. Note that there are four smiley-face leaves in the tree. This means there are four different ways to get a proof, which means there are four different sets of variable assignments. Finally, let's look at a list predicate.

```member(X, [X|_]).
member(X, [_|T]) :- member(X, T).
```

This is familiar to us from the Prolog notes. When we query with `member(X, [a, b, c])` we get that `X = a`. When we query with `member(d, [a, b, c])` we get failure. Much of these notes were adapted from Learn Prolog Now!, a free online textbook.

Intro to AI material by Joshua Eckroth is licensed under a Creative Commons Attribution-ShareAlike 3.0 Unported License. Source code for this website available at GitHub.