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
iii. Square 1.1 does not have a mine
~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)
~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
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
<answer to be added here>
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.
"a "s dead(duck, s) => dead(duck, resultof(a, s))
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)))