Resolution in prolog

Question

What exaclty is resolution in prolog and how does it enables Prolog to obtain the following answer:
?- sublist([b,c],[a,b,c]).
true

Answer 1

As expressed, this looks like a homework question, and there is missing information, specifically, the definition of sublist/2.

Having said that, you did ask a good computer science question, namely, what exactly is "resolution" in Prolog and, more to the point, why is it called "resolution" in the first place.

If you're not used to reading sequent notation, what follows is going to need a little bit of explanation. A sequent is a formula of this form:

$$A_1,\ldots,A_p \vdash B_1,\ldots,B_q$$

where the $A_i$ and $B_i$ are logical formulas. The turnstile symbol, $\vdash$, is pronounced "entails".

A good intuitive sense of what this sequent means is that the conjunction of everything on the left-hand side of the turnstile, $A_1 \land \cdots \land A_p$, logically entails the disjunction of everything on the right-hand side of the turnstile, $B_1 \lor \cdots \lor B_q$.

The exact form of a sequent may in general depend on the logic being studied; for example, some logics only use one formula on the right-hand side of the turnstile. Or the formulas may have special forms.

A rule is a line with zero or more sequents above it and one sequent below it. Here is an example of a rule, the "$\land$-introduction" rule in propositional logic:

$$\frac{\Gamma \vdash A \quad\quad \Delta \vdash B} {\Gamma,\Delta \vdash A \land B}$$

If the assumptions $\Gamma$ entail the conclusion $A$, and the assumptions $\Delta$ entail the conclusion $B$, then the combined assumptions $\Gamma,\Delta$ entail the conclusion $A \land B$.

This is the resolution rule in logic:

$$\frac{\Gamma \vdash \Sigma, c \quad\quad \Delta \vdash \Xi, \neg c} {\Gamma,\Delta \vdash \Sigma,\Xi}$$

Making the disjunctions explicit, you can think of it this way:

$$\frac{\Gamma \vdash A_1\lor \cdots \lor A_p \lor c \quad\quad \Delta \vdash B_1\lor \cdots \lor B_q \lor \neg c} {\Gamma,\Delta \vdash A_1\lor \cdots \lor A_p \lor B_1\lor \cdots \lor B_q}$$

If it helps, you can think of what is going on in a classical propositional logic. By the law of the excluded middle, $c$ is either true or false. If it's false, then all of $B_1, \ldots, B_q$ might be false, but at least one of $A_1, \ldots, A_p$ must be true. Similar reasoning applies if $c$ is true.

Now to get the intuition on what resolution in Prolog means, we're going to look at a cut-down version of Prolog with no explicit disjunction and no negation. Every clause is a Horn clause, which of this form:

p :- q,r,s.

The comma symbol means logical "and", and the :- should be thought of as an implication pointing to the left. If we can prove q, r, and s, then we can conclude p. Or, to put it another way, $\left( q \land r \land s \right) \Rightarrow p$. Or, to put it yet another way, $\neg q \lor \neg r \lor \neg s \lor p$.

You can think of a cut-down-Prolog program as being essentially in conjunctive normal form. All of the clauses are true, so they are logically "and-ed" together. Each clause is an implication with one conclusion, so it is logically an "or".

To prove $p$ in this system, you can essentially do it by contradiction: you assume $\neg p$ and try to show that the program (which, remember, is in CNF) is unsatisfiable.

Applying logical resolution to $\neg p$ and $\neg q \lor \neg r \lor \neg s \lor p$ gives $\neg q \lor \neg r \lor \neg s$. So now, to prove that this is unsatisfiable, we can perform resolutions with other clauses that have $q$, $r$, or $s$ positive, that is, they are the left-hand side of some Prolog clause.

What actually happens in Prolog is the same thing, only without all the negation: we prove $p$ by trying to prove $q$, $r$, and $s$.

What I can hope you can see here is why it's called "resolution", because Prolog's inference rules play the same role as predicate logic resolution.

Prolog's actual inference rule is known as "selective linear definite clause resolution, with negation-as-failure", or SLDNF resolution for short. It deals with the fact that pure Prolog is a first-order predicate system with a full complement of logical operators, so you need to deal with unification and variable substitution and negation-as-failure.

Extra-logical operators such as the cut are another issue entirely. Coming up with formal semantics for Prolog was something of an industry in the 80s and 90s because of this. I think we have now decided that Prolog has an operational semantics, and if you need something that is more "logical", you need a "purer" logic language than Prolog. But still, the basic mechanism is SLDNF resolution.