In order to formulate logical statements about this game, we define a number of expressions:
The cards are each represented with a two-character abbreviation: a letter for the category (a, b and c) and a number (1-4) for which card in the category it is. This is the set cards = {a1, a2, a3, ... c2, c3, c4}
The first card of each set is initially physical, and this is represented with the set phys, which is a subet of cards. phys = {a1, b1, c1}
The other part of the set cards, which are the initially blank ones, form the set nonPhys. nonPhys = {a2, a3, a4, b2, b3, b4, c2, c3, c4}
The cards are can also be referred to as being from a category, so the following sets are defined: setA = {a1, a2, a3, a4}; setB = {b1, b2, b3, b4}; setC = {c1, c2, c3, c4}
We have our three players or agents, which we name X, Y and Z. agents = {X, Y, Z}
Apart from these, we will need a number of predicates to describe game situations. We use the following:
Agent A has card x1: has(A, x1)
It is agent A's turn: turn(A)
Agent A asks agent B for card x1: ask(A, B, x1) Where A and B may not be equal.
Agent A has n cards: hasNr(A, n)
Agent A has n cards from the set nonPhys: hasBlank(A, n)
A reminder: The expression N(f) from temporal logic means f will be true in the next time step, defined here as the next turn.