# Mine Sweeper

The game of mine sweeper is played with a rectangular grid of squares.  Some of the squares contain mines, but initially all the squares are covered so that you cannot see where the mines are.  You are told how many mines there are.

Some action, e.g. left-click with the mouse lets you “step” on a square.  You may step on any covered square.  If the square you step on contains a mine, the game is over and you lose.  If the square does not contain a mine, it is uncovered.  An uncovered square shows you a count of how many adjacent squares have mines.  For instance, here is a board after two squares were stepped on: The following diagram shows a placement of mines that would result in the counts shown above. Another action, e.g. right click, can be used to mark a square as having a mine.  If all the mines are marked and all the other squares stepped on, the game is over and you win.

For the following problems, we will assume we have a very small board, with only one column and three rows.

1. Propositional logic
1. Express the following in propositional logic:

i.

If square 1,2 has a count of 1 then
(square 1,1 does not have a mine and square 1,3 has a mine
or square 1,1 has a mine and square 1,3 does not have a mine)

ii.         Square 1,2 has a count of 1

iii.         Square 1.1 does not have a mine

1. Convert  a.i above to the form (_ v _ v …) ^ (_ v _ v  …) ^ …i.e. to an AND of  ORs
2. Use your answers to b and a.ii and a.iii to prove that square 1,3 has a mine., using only resolution as an inference rule.  Use regular resolution, not resolution refutation.

1. First order logic
1. .  You may assume that objects 0, 1, 2, … , have been defined as representing the non-negative integers.  You may assume that the relations (predicates) greater, less, and equals have been defined, as well as the functions predecessor (predecessor(n) is n-1) and successor (successor(n) is n+1)..   You may use additional predicates and functions as long as you provide definitions for them in FOL in terms of the predicates and functions listed above.

i.         Choose a ways to represent the fact that there is a mine in a given square and that the count of a given square is n.  Explain the representation in English

Express the following (ii and iii) succinctly and formally in first order logic.  Situation calculus is not needed

ii.         Two squares are neighbors if their y-coordinates differ by 1

iii.         The count at a square is the number of neighbors that contain mines.

iv.         Give a proof by backchaining resolution refutation that if the count at a square is 1 and the cell above it has a mine, then the cell below it does not have a mine.

1. Situation calculus

Here is a puzzle:  A farmer has three items:  a fox, a duck, and some corn.  He wants to cross a river, but he can take at most one of these three items into the boat with him at a time.  If he leaves the fox alone with the duck the fox will eat the duck.  Similarly for the duck and the corn.  How can he get himself and all the items across?

You do not need to solve this puzzle, just to write parts of it in FOL, as follows:

We will name the near side of the river near and say other(near) means the far side.  Of course, other(other(near)) = near..  So, to say that the duck is on  the far side in state s, we write at(duck, other(near), s).  The only actions involve crossing the river:  crossFrom(near, duck) is the action of taking the duck from the near side to the far side.  If the farmer crosses alone, the action is crossFrom(near, farmer).  The predicates dead(duck, s) or dead(corn, s) mean that the duck or corn are not in existence in state s (i.e. they have been eaten).

a.     Write in FOL, using situation calculus, the statement that if the fox and the duck are on a side of the river and the farmer is not on that side, then in the next state the duck will be dead.

b.     Similarly, write an axiom that says once an item is dead it stays dead, no matter what the farmer does.

c.     Write effect and frame axioms that  describe how crossFrom affects the at predicate.