?- has(U,S),\+((has(V,T),T>S)).
U = mark,
S = 6 ;
false.

The prefix operator \+ read as not. Since what we must disprove is a conjunction, expressed by the infix operator ,, those double parenthesis are required.

You should be aware, when using it, that it is a restricted form of negation, so called negation as failure, made possible by the closed world assumption that is implicit in Prolog semantics.

Alternatively, doing exactly the same

max(U,S) :- has(U,S),notanybetterthan(S).

notanybetterthan(S) :- has(_,T),T>S,!,fail.
notanybetterthan(_).

or

max(U,S) :- has(U,S),\+anybetterthan(S).

anybetterthan(S) :- has(_,T),T>S.

edit

As noted by @WillNess, the syntax I used was imprecise. Indeed the double parenthesis are a consequece of \+ seen as a functor, not as operator. Adding a space after the symbol we can write instead

?- has(U,S),\+ (has(V,T),T>S).

You can use the standard predicates findall/3 and keysort/2:

| ?- findall(Value-Name, has(Name, Value), Pairs),
     keysort(Pairs, SortedPairs).

Pairs = [5-steve, 6-mark, 4-craig],
SortedPairs = [4-craig, 5-steve, 6-mark]
yes

You want the last pair in the SortedPairs list. Simply walk the list until you reach its last element. I will leave that to you to write a last(List, Last) predicate.

Update

Carlo's solution is nicely idiomatic (+1). But it's also O(n^2). My solution (including the missing last/2 predicate) is O(2*n + n*log(n)). On the other hand, it hits the garbage collector slightly more due to the temporary lists that are created. If we have only the tree facts in the OP, Carlo's solution is ~3x faster. With ~100 facts, both solutions take roughly the same amount of time (note that exact numbers depend on the used Prolog system). For a large number of facts, the differences in complexity become more and more apparent.

Give this a go:

has(steve, 5).
has(mark, 6).
has(craig, 4).

?- findall(has(X, Y), has(X, Y), Z), maxhas(Z, has(Who, Max)), write([Who, Max]).

maxhas([has(X, Y)], has(X, Y)).
maxhas([has(_, Y)|Hs], has(A, B)) :- maxhas(Hs, has(A, B)), B >= Y.
maxhas([has(X, Y)|Hs], has(X, Y)) :- maxhas(Hs, has(_, B)), B < Y.

I get:

[mark, 6]Yes.