How to create arithmetic and disequality constraints in Prolog

I'm brand new to Prolog, and I'm interested in converting the following word problem into (SWI) Prolog:

There are 4 children: Abe, Dan, Mary, and Sue. Their ages, in no particular order, are 3, 5, 6, and 8. Abe is older than Dan. Sue is younger than Mary. Sue's age is Dan's age plus 3 years. Mary is older than Abe.

So far I've come up with

child(X) :-
    member(X, [3,5,6,8]).

solution(Abe, Dan, Mary, Sue) :-
    child(Abe),
    child(Dan),
    child(Mary),
    child(Sue),
    Abe > Dan,
    Sue < Mary,
    Sue == Dan+3,
    Mary > Abe,
    Abe \== Dan,
    Abe \== Mary,
    Abe \== Sue,
    Dan \== Mary,
    Dan \== Sue,
    Mary \== Sue.

But running the query

?- solution(Abe, Dan, Mary, Sue)

I just get false. As a side question, will Prolog perform brute force search for solutions, or is there some machinery which can solve this (sort of) problem in better than O(n!) ?

The result I want is Abe = 5, Dan = 3, Mary = 9, Sue = 6.

Solution

Arithmetic constraints over integers, such as the constraints in this puzzle, are best expressed with your Prolog system's CLP(FD) constraints.

For example, in SICStus Prolog, YAP or SWI:

:- use_module(library(clpfd)).

ages(As) :-
        As = [Abe,Dan,Mary,Sue],    % There are 4 children: Abe, Dan, Mary, Sue
        As ins 3\/5\/6\/8,          % Their ages are 3, 5, 6 and 8
        all_different(As),
        Abe #> Dan,                 % Abe is older than Dan
        Sue #< Mary,                % Sue is younger than Mary
        Sue #= Dan + 3,             % Sue's age is Dan's age plus 3 years
        Mary #> Abe.                % Mary is older than Abe

Sample query and its result:

?- ages([Abe,Dan,Mary,Sue]).
Abe = 5,
Dan = 3,
Mary = 8,
Sue = 6.

We see from this answer that the puzzle has a unique solution.

Note that no search whatsoever was necessary to obtain this answer! The constraint solver has deduced the unique solution by a powerful implicit mechanism called constraint propagation, which is the key advantage of CLP systems over brute force search. Constraint propagation is successfully used in this example to prune all but one remaining branch of the search tree.