# Mine Sweeper

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)

c12-1 => (~m11 ^m13 v   m11  ^ ~m13)

ii.         Square 1,2 has a count of 1

c12-1

iii.         Square 1.1 does not have a mine

~m11

1. Convert  a.i above to the form (_ v _ v …) ^ (_ v _ v  …) ^ …i.e. to an AND of  Ors

~c12-1 v (~m11 ^ m13 v   m11  ^ ~m13)

= (~c12-1 v ~m11 v   m11)^ (~c12-1 v ~m11 v   ~m13)^ (~c12-1 v m13 v   m11)^

(~c12-1 v m13 v   ~m13)

= (~c12-1 v ~m11 v   ~m13)^ (~c12-1 v m13 v   m11)

1. 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.

Clauses:

c12-1
~m11

~c12-1 v ~m11 v   ~m13

~c12-1 v m13 v   m11

c12-1         ~c12-1 v m13 v   m11

m13 v  m11

m13 v  m11      ~m11

m13

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 way to represent the facts that there is a mine in a given square and that the count of a given square is n.  Explain the representation in English

M(S(y)) represents “there is a mine in square (1, y).”

C(S(y, n)  means “the count of square (1, y) is n”

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

"y neighbors(S(y),S(succ(y))) ^  neighbors(S(Succ(y)), S(y))

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

Cu(S(y), n) means the count at square(1, y) counting only mines on the square above it is n

"y  M(S(successor(y)) ó Cu(S(y), succ(0))   (succ(0) is 1)

"y  ~M(S(successor(y)) ó Cu(S(y)), 0)

"y  M(S(y)) ó\$ zC(S(successor(y)), succ(z)) ^ Cu(S(successor(y)), z)

"y  ~M(S(y)) ó \$ zC(S(successor(y)), z) ^ Cu(S(successor(y)), z)

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.

A typo!  I meant backchaining modus  ponens , but we will accept either backchaining gmp or reso;lution refutation

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.

" a " s " x  at(duck, x, s) ^ at(fox, x, s) ^ ~at(farmer, x, s) => dead(duck, resultof(a, s))

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.

"side" item " s  at (farmer, side, s)  ó

at (farmer, other(side),resultof (crossFrom(side, item), s))

"side" item " s  at (item, side, s)  ó

at (item, other(side),resultof (crossFrom(side, item), s))

"side" item1 " item2 " s  ~(item1 = item2) ^ ~(item1=farmer) =>

(at (item1, side, s)  ó

at (item1, side,resultof (crossFrom(side, item2, s)))