Logic In Game Playing Communication

Knowledge Interchange Format

KIF is a standard for programmatic exchange of knowledge represented in relational logic.

  • Variables are prefixed with ? (e.g. ?x)
  • Case-indepedent.

Game Description Language (GDL)

We use GDL to describe games (used in global competitions).

GDL lists 'facts' and 'rules':


  • role(r) - r is a player in the game
  • init(f,b) - tells us that f starts as b
  • true(f) - f is true currently
  • does(r,a) - player r does action a
  • next(f) - f is true in the next state
  • legal(r,a) - it is legal for r to do a currently
  • goal(r,v) - r gets goal value v in the current state
  • terminal - current state is a leaft node
  • distinct(s,t) - s and t are syntactically different
  • init(control(x)) - player x starts off with control of the game

Rule Examples:

  • legal (P, mark(M,N)) <= true(cell(M,N,b)) ^ true(control(P)) - it's a legal move if the cell is blank and it's P's turn
  • next(cell(M,N,x)) <= does(xplayer, mark(M,N)) - the next move is set as this iff player x marks that cell

In competitions we usually use pure logic (no built in assumptions). We hence replace words like 'mark' and 'cell' with random nonsense words - it's just as easy for the computer, but much harder for a human to understand.

Communication Protocol

Manager sends START message to players
- Match ID: the name of the game
- Role: the name of the role you are playing (e.g. xplayer or oplayer)
- Game description: the axioms describing the game
- Start/play clock: how much time you have before the game begins/per turn
Manager sends PLAY message to players
Prior moves is a list of moves, one per player
- The order is the same as the order of roles in the game description
- e.g. ((mark 1 1) noop)
- Special case: for the first turn, prior moves is nil
Players send back a message of the form MOVE, e.g. (mark 3 2)
When the previous turn ended the game, Manager sends a STOP message


Game descriptions are logically incomplete - they do not uniquely specify the moves of the players. Every game description contains complete definitions for legality, termination, goal values and update - in terms of 'true' and 'does'. Meaning at every state every player can determine the above and update the state.

Dependency Graphs

The dependency graph for a set of clauses is a directed graph for a set of clauses is a directed graph in which the nodes are the predicates from the heads and bodies, and there's an arc from a node a to a node b whenever a is in the body with b in its head.

If there's a cycle then the set is recursive.



Safe clause
A clause where every variable in it appears in some positive subgoal in the body.


  • Safe Rule: r(X,Y) <= p(X,Y) ∧ q(Y,Z) ∧ ¬r(X,Z)
  • Unsafe Rule: r(X,Z) <= p(X,Y) ∧ q(Y,X)

All rules in GDL must be safe, and hence all facts must be variable free (they have no body).

Stratified Set of Rules
A set of rules with no recursive cycles involving negation in the dependency graph.

All game descriptions in GDL are stratified.

These two things guarantee finiteness.

Logic Problems

Logic problems are finite collections of clauses (clauses are the following):

  • Facts are atoms
  • Rules are head <= body
  • Body = sentence using ^, v, and literals
  • Head = atom

e.g. Likes Milk <= Is a Cat

To compute logical consequences you need to do the following:

  1. unification (use substitutions in order to match two expressions)
  2. resolution steps (a single derivation step)
  3. derivations (compute the result of a query)


A Substitution is a finite set of replacements of variables by terms:

\begin{align} p(X,X,Y,Z){X/a,Y/f(b),V/W} \rightarrow p(a,a,f(b),Z) \end{align}

i.e. p(set/expression){replacements} -> p(newset/newexpression)


Two expressions are said to be unifiable is a substitution exists such that both of them end up with the same new expression.


\begin{equation} mark(M,N){M/1, N/3, X/3} = mark(1,X){M/1, N/3, X/3} = mark(1,3) \end{equation}

The substitution {M/1, N/3, X/3} is hence called a unifier.


\begin{align} mark(X,X) \text { and } mark(1,3) \text{ are not unifiable} \end{align}

Most General Unifiers

A substitution a is said to be more general than a substitution b iff there is a substitution c such that $a \circ c = b$.


\begin{align} a = {M/1, N/X} \text{ and b = } {M/1, X/O} \text{ and c = } {X/O, N/X} \end{align}

a is more general than b, because a.c = b

A substitution a is said to be the most general unifier (mgu) of two expressions iff it is more general than any other unifier.

If two expressions are unifiable then they have an mgu that is unique (up to variable permutation).

Resolution Steps

Given a query (of the form "?- legal(xplayer,M)")
Given some clauses.

Let A <= B1 and B2 and B3 and …. and Bn be a 'fresh' variant of a clause
Let σ be the mgu of L1 and A

Then applying the mgu to the query and the fresh variant of the clause is a resolution step (matches more parts of them).

σ = {P5/xplayer,M/mark(M5,N5)}
Clause: legal(P5,mark(M5,N5)) <= true(cell(M5,N5,b)) ∧ true(control(P5)) → legal(xplayer,M) <= true(cell(M5,N5,b)) true(control(xplayer))

(In logic programming, a fresh variant of a clause is a rewriting of the clause using new variables. The use of fresh variants is necessary to avoid the variables of a rule to be incorrectly bound to the values of variables that are used somewhere else in the program).

Essentially we're trying to substitute things in the query and the clauses until we find a state where a clause matches the query.

Query Answering

A sequence of resolution steps is called a derivation, and a successful derivation ends with an empty query, and a failed derivation ends with a query to which no clause applies.

The answer substitution (what we compute with a successful derivation) is obtained by composing the mgu's of each step (and restricting the result to the variables in the original query).



If, in the above, we do {P/xplayer, M/mark(M5,N5)} then we get
"?- legal(xplayer,mark(M5,N5)"
"legal(xplayer,mark(M,N)) <= true(cell(M,N,b)) ∧ true(control(xplayer))"

then {M5/1, N5/1} gives us:
"?- legal(xplayer,mark(1,1)"
"legal(xplayer,mark(M,N)) <= true(cell(M,N,b)) ∧ true(control(xplayer))"

The query hence matches and is understood.

Query Answering with Negation

Query Answering with Disjunction

A clause with a disjunction "A <= B ∧ (C ∨ E) ∧ D"
Is logically equivalent to the conjunction of the clauses
"A <= B ∧ C ∧ D"
"A <= B ∧ E ∧ D"