- A set of valid board configurations.
- An initial board configuration.
- A relationship defining valid transitions between board configurations.
- A score function for final configurations.

dffinal_configurations( configurations :set, transitionssubsetconfigurations^{2}) = {pinconfigurations |notExistqinconfigurations ((p,q)intransitions)}

Now we can define the collection of all possible abstract games, where we require that all configurations can be reached from the initial configuration:

dfabstract_games = { ( configurations :set, initialinconfigurations , transitionssubsetconfigurations^{2}, score :functionfromfinal_configurations(configurations, transitions)tointeger ) | configurations = {qinconfigurations | (initial, q) in transitions^{*}} }

Now we can define the set of all valid games as sequences of configurations, where the first configuration is the initial configurations and the last configuration one of the final configurations. All pairs of consecutive configurations must be valid transistions. This can be defined with:

dfvalid_games((configurations, initial, transitions, score)inabstract_games) = { (p_{0}, .., p_{n})inconfigurations^{n}| p_{0}= initialandp_{n}in final_configurations(configurations, transitions)andForall0<i<=n ((p_{i-1}, p_{i})intransitions) }

dfplaying_strategies((configurations, initial, transitions, score)inabstract_games) = {functionfromconfigurations - final_configurations(configurations, transitions)toconfigurationssubsettransitions }

dfplayed_game(gameinabstract_games, strategy_{0}inplaying_strategies(game), strategy_{1}inplaying_strategies(game)) = (p_{0}, .., p_{n})invalid_games(game)whereForall0<i<=n (p_{i}= strategy_{i mod 2}(p_{i-1}) )

dfoutcome(gameinabstract_games, (p_{0}, .., p_{n})invalid_games(game)) = score(p_{n})where(configurations, initial, transitions, score) = game

dfdrawless(gameinabstract_games) =Forallplayed_game in valid_games(game) (not(outcome(game, played_game) = 0))

dfsuper_strategies(gameinabstract_games) = { strategyinplaying_strategies(game) |Forallother_strategyinplaying_strategies(game) - {strategy} ( outcome(played_game(strategy,other_strategy)) >= 0andoutcome(played_game(other_strategy,strategy)) >= 0) }

dfstrategy_quality(gameinabstract_games, strategyinplaying_strategies(game)) =Minimum{ outcome(played_game(strategy,other_strategy)) + outcome(played_game(other_strategy,strategy)) | other_strategyinplaying_strategies(game) - {strategy} }

dfminimal_winning_patterns(points :set) = { patternssubsetpowerset(points) |Forallp_{1}, p_{2}inpatterns (p_{1}= p_{2}ornot(p_{1}propersubsetp_{2})) }

Now the set of all strong positional games can be characterized with the following:

dfstrong_positional_games = { (points :set, wps_{1}, wps_{2}) | wps_{1}inminimal_winning_patterns(points)andwps_{2}inminimal_winning_patterns(points) }

dfsymmetric_strong_positional_games = { (points, wps_{1}, wps_{2})instrong_positional_games | wps_{1}= wps_{2}}

dfexcluding_strong_positional_games = { (points, wps_{1}, wps_{2})instrong_positional_games |Forallwp_{1}inwps_{1}, wp_{2}inwps_{2}(not(wp_{1}intersectionwp_{2}= {})) }

dfwinning_positions(points :set, wpinminimal_winning_patterns(points)) = { winsubsetpoints |Existswinwp (wsubsetwin) }

Now we can define all configurations for a strong positional game:

dfspg_configurations((points, wps_{1}, wps_{2})instrong_positional_games) = { (ps_{1},ps_{2})in(powerset(points))^{2}| ps_{1}intersectionps_{2}= {}and(count(a) =count(b)orcount(ps_{1}) =count(ps_{2}) + 1)andnot( ps_{1}inwinning_positions(points, wp_{1})andps_{2}inwinning_positions(points, wp_{2}))

Next we can define all transtions for a strong positional game:

dfspg_transitions(pfginstrong_positional_games) = { ((fps_{1},fps_{2}),(tps_{1},tps_{2}))inspg_configurations(game) | fps_{1}subsettps_{1}andfps_{2}subsettps_{2}andcount(tps_{1}) +count(tps_{2}) =count(fps_{1}) +count(fps_{2}) + 1 }

Last we need to define the scoring function:

dfspg_score((points, wps_{1}, wps_{2})instrong_positional_games) = { ((ps_{1},ps_{1}, value)inspg_configurations(game)x{-1,0,1} | value =ifps_{1}in winning_positions(points, wps_{1})then1elifps_{2}in winning_positions(points, wps_{2})then-1else0fi}

dfspg_game(pfginstrong_positional_games)inabstract_games = (spg_configurations(pfg), ({},{}), spg_transitions(pfg), spg_score(pfg))

dftic_tac_toe = ( (1,2,3,4,5,6,7,8,9), rows, rows )whererows = {{1,2,3},{4,5,6},{7,8,9} ,{1,4,7},{2,5,8},{3,6,9} ,{1,5,9},{3,5,7}}

dfgroups(points :set, neighbourssubsetpoints^{2}) = { groupsubsetpoints |Foralla,bingroup ((a,b)in(neighboursintersectiongroup^{2})^{*}) }

dfconnection_games( points :set, neighbourssubsetpoints^{2}) = { (points, wps_{1}, wps_{2})instrong_positional_games | wps_{1}subsetgroups(points, neighbours)andwps_{2}subsetgroups(points, neighbours) }

dfmaximal( gamesinconnection_games( points :set, neighbourssubsetpoints^{2})) = (points, wps_{1}, wps_{2})ingamessuchForall(points, owps_{1}, owps_{2})ingames (owps_{1}subsetwps_{1}andowps_{2}subsetwps_{2})

dfHex_points(sizeinNatural | size < 1) = { (x,y)in{0,..,size-1}^{2}}

The neighbours relationship on the points can be defined with:

dfHex_neighbours(sizeinNatural | size < 1) = { ((x_{1},y_{1}),(x_{2},y_{2}))inHex_points(size)^{2}| (x_{1}-x_{2})^{2}+ (y_{1}-y_{2})^{2}- (x_{1}-x_{2})(y_{1}-y_{2}) = 1 }

From this the game of Hex can be defined as a connection game in the following way:

dfHex_game(sizeinNatural | size < 1) = maximal({ (points, wps_{1}, wps_{2})inconnection_games(Hex_points(size), Hex_neighbours(size)) |Forallwpinwps_{1}(Existx_{1}((x_{1},0)inwpandExistx_{2}((x_{2},size-1)inwp)andForallwpinwps_{2}(Existy_{1}(0,(y_{1})inwpandExisty_{2}(size-1,(y_{2})inwp) })

In this definition we start with a cube of points and take the points that are on the intersection of a plane, that goes right through the middle of six of the ribs, creating the desired hexagonal set of points. The coordinates with which the points are defined have a degree of freedom of only two. This means that each of the elements can always be calculated if the other two are known.dfHavannah_points(sizeinNatural | size < 1) = { (x,y,z)in{1-size,..,size-1}^{3}| x + y + z = 0 }

We can define the distance between two points as the length of the shortest path between the points. We can do so using:

The sum of absolute differences of the coordinates is always even, because the degree of freedom is two. The points with the same distance to a given point are on the imaginary hexagon of which the corners are on the lines through this point and on the given distance.dfHavannah_distance(sizeinNatural | size < 1, (x1,y1,z1)inHavannah_points(size), (x2,y2,z2)inHavannah_points(size)) = ( |x1-x2| + |y1-y2| + |z1-z2| )/2

With this definition it is also possible to define the neighbour relation:

dfHavannah_neighbours(sizeinNatural | size < 1) = { (p,q)inHavannah_points(size)^{2}| Havannah_distance(size,p,q) = 1 }

The Havannah groups are defined with:

dfHavannah_groups(sizeinNatural | size < 1) = groups(Havannah_points(size), Havannah_neighbours(size))

And a function that returns all neighbours of a point:

dfHavannah_neighbours_of(sizeinNatural | size < 1, pinHavannah_points(size)) = { qinHavannah_points(size) | (p,q)inHavannah_neighbours(size) }

With this definition we have established the board and some of its properties.dfHavannah_corner_points(sizeinNatural | size < 1) = { pinHavannah_points(size) |count(Havannah_neighbours_of(size, p)) = 3 }dfHavannah_side_points(sizeinNatural | size < 1) = { pinHavannah_points(size) |count(Havannah_neighbours_of(size, p)) = 4 }

dfHavannah_bridges(sizeinNatural | size < 1) = { groupinHavannah_groups(size) |count( groupintersectionHavannah_corner_points(size) ) = 2 }

dfHavannah_forks(sizeinNatural | size < 1) = { groupinHavannah_groups(size) |count({ { binHavannah_side_points(size) | (s,b)in(Havannah_side_points(size)^{2}intersectionHavannah_neighbours(size))^{*}} | sin(groupintersectionHavannah_side_points(size)) }) = 3 }

Finanlly, we look at the cycles. The definition of the set of all positions that contain a cycle:

dfHavannah_cycles(sizeinNatural | size < 1) = { {p_{0},..,p_{n-1}}inHavannah_groups(size) |Forall1<=i<n ( Havannah_distance(size, p_{i},p_{(i+1) mod n}) = 1andHavannah_distance(size, p_{i},p_{(i+2) mod n}) >= 2 ) }

From this the game of Havannah can be defined as a connection game in the following way:

dfHavannah_game(sizeinNatural | size < 1) = (Havannah_points(size), wps, wps)inconnection_games(Havannah_points(size), Havannah_neighbours(size))wherewps = Havannah_cycles(size)unionHavannah_bridges(size)unionHavannah_forks(size)

home and email