The rules of the game are formalized with the following expressions:
Each card is owned by a player: FORALL(x|cards): EXISTS(a|agents): has(a, x)
A card can only be owned by one player: FORALL(x|cards): FORALL(a, b|agents): has(a,x)^a!=b -> !has(b, x)
At the start of the game each player has 4 cards: FORALL(A|agents): hasNr(A, 4) during the first time step (where no card has yet been asked).
A player has to own at least one card from a set he asks for a card from: FORALL(A|agents): FORALL(x\setA): ask(A, x) -> (EXISTS(y|setA): has(A, y) ^ !has(A, x) )
When agent A asks agent B for card x and B has this card, B must give it to A and A keeps the turn: FORALL(A,B|agents): FORALL(x|cards): ask(A, B, x)^has(B, x) -> N(C(has(A, x)^turn(A)))
When agent A asks agent B for card x and B does not have it, B gets the turn: ask(A, B, x)^!has(B, x) -> N(turn(B)^C(!has(B, x))) Note that with three players, this automatically means that the third player (the one not asking and not being asked) must have the card as A could not ask for it if he had it and B does not have it.
Once a player has all four cards of a category, they can no longer be asked for: FORALL(a|agents): has(A, a1)^has(A, a2)^has(A, a3)^has(A, a4) -> [](FORALL(B|agents)!(ask(B, a1) v ask(B, a2) v ask(B, a3) v ask(B, a4)) And the same for the other categories, with the a's replaced with b's and c's.
These are the rules required to reason about the changing knowledge. They are not sufficient to model the entire course of a game, but that falls outside the scope of this project as there was not enough time and manpower.