A logic-programming engine answers a query by repeatedly selecting a goal, matching it against a fact or rule head, and replacing it with the rule's premises. This proof-search process is based on resolution.

For the goal

grandparent(alice, carol)

and rule

grandparent(X, Z) :- parent(X, Y), parent(Y, Z)

unification yields $X=alice$ and $Z=carol$, leaving the subgoals

parent(alice, Y)
parent(Y, carol)

A fact may bind Y = bob, after which the remaining goal can succeed.

When several rules or facts might match, the engine explores alternatives. If a chosen branch later fails, backtracking restores an earlier choice point and tries another alternative.

The declarative meaning of the rules and the operational search strategy are distinct. Two logically equivalent rule sets can behave very differently under a depth-first search order; a poorly ordered recursive rule may even diverge before reaching an available solution.

Understanding resolution and backtracking therefore explains both the expressive appeal and operational surprises of logic programming: execution is proof search, but the order in which proofs are searched still matters for performance and termination.