How could I express this knowledge in SWI-Prolog?

Question

I never worked with swi-prolog and I'm having trouble figuring out how to express a bit more complicated knowledge in it. I want to express this in swi-prolog:

∃x∃yTile(t,x,y,r) ∧ ∀a∀bTile(t,a,b,r) => a=x, b=y

or

∃x∃yTile(t,x,y,r) ∧ ∀a∀bTile(t,a,b,r) => a!=x; b!=y

Basically what I want to express that there can be a tile of type 't' and position x and y at round 'r' and for all tiles if their position is the same as x and y it means it is the same tile and only one tile of that type exists in the world or the opposite could be true and there are multiple tiles of the same type.

The closest I could find and write is this:

find_tiles(T, X, Y, R) :-
    tile(T, X, Y, R),
    forall(
        (tile(T, A, B, R), A = X, B = Y),
        true
    ).

But I'm not really sure it would work, any help or resources to learn would be very appreciated.

Answer 1

To express that

there can be a tile of type 't' and position x and y at round 'r' and for all tiles if their position is the same as x and y it means it is the same tile and only one tile of that type exists in the world

you would have to test in the Action part of the forall/2 whether each comforming tile has the same coordinates:

find_tiles(T, X, Y, R) :-
    tile(T, X, Y, R),
    forall(
        tile(T, A, B, R),
        (A = X, B = Y)   % here the test
    ).

Alternatively you can use setof/3:

find_tiles(T, X, Y, R):-
 setof([X,Y], tile(T,X,Y,R), [[X,Y]]).