Answers

- Propositional logic
- 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

- 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)

- 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

- First order logic
- . 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

<answer to be added here>

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

"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)))