1) (agents and environment simulators - 5%):
For each of the following domains, which type of agent is appropriate
(table lookup, reflex, goal based, or utility based). Also, indicate the
type of environment:
a) An agent that plays Poker.
b) A fully autonomous car.
c) An internet shopping agent specializing in purchasing kitchen appliances.
d) An agent that can play 3x3 tic-tac-toe.
e) An agent that can play Gomoku
ANSWERS:
This question is somewhat vague, and there is more than one answer,
a) Poker: Need a utility based agent, as the need is to maximize something (money)
and much too large a state to use just reflex.
The environment is stochastic (cards deal, can be modeled as quasi-deterministic),
partially observable, non-episodic, (mostly) discrete (except for perhaps amounts of money),
multi-agent, and can be seen as static.
b) Even more complicated utility based agent needed. Environment is stochastic, partially observable,
non-episodic, continuous, multi-agent, and dynamic. As bad hard as can be!
c) Utility based agent. Environment is stochastic, partially observable, dynamic, multi-agent
but can be modeled as single agent, (mostly) discrete, and non-episodic.
d) Easily done by a goal-based agent, but simple enough to be done by reflex agent or even
table lookup. Environment is deterministic, complete information, discrete, static, can be seen as episodic,
and multi-agent. One of the easiest possible for zero-sum games.
e) Goal-based agent (state too large for table lookup and optimal rules unknown, so requires search).
Same evironment type as for tic-tac-toe, but state space size makes it harder.
2) (Search - 20%):
Show the run of the following algorithms on the setting of question 6
below, where the agent starting at V0 needs to save as many people as possible,
where costs are as defined in assignment 1.
Assume that h(n) is the heuristic defined in class (based on number of
people in the groups that cannot be saved if considered in isolation).
a) Greedy search (f(n) = h(n)), breaking ties in favor of states where the
higher node number.
b) A* search, (f(n) = g(n)+h(n)), breaking ties as above.
c) Simplified RTA* with a limit of 2 expansions per real action, breaking ties as above.
d) Repeat a-c but using h'(n) = 2*h(n) as the heuristic. Is h'(n) admissible?
ANSWER:
First, the state representation. We will use the vector: (Loc, People at V1, People at V3, Carrying, Safe, Time, Term)
to indicate state, for clarity, despite the redundancies. The heuristic is: number of people which can no
longer be saved in this state if considered in isolation.
The initial state and only one on the agenda initially is:
S0: (V0, 1, 2, 0, 0, 0, F) g=0, h=2, h'=4 (cannot save people at V3)
S0 is retrieved, and is not a goal state so is expanded to add:
S1: (V0, 1, 2, 0, 0, 0, T) g=3, h=0, h'=0 by terminate action
S2: (V1, 0, 2, 1, 0, 3, F) g=0, h=3, h'=6 by moving to V1 (can no longer save anybody)
S3: (V2, 1, 2, 0, 0, 1, F) g=0, h=2, h'=4 by moving to V2 (can still save people at V1)
The rest of the run depends on the algorithm.
a) Greedy search takes S1 as it has the lowest h (also with h'), sees that this is a goal state, and terminates.
b) Running with heuristic h, both A* and RTA* pick S3 because F(S3)=0+2=2, and it is not a goal so is expanded:
S4: (V2, 1, 2, 0, 0, 1, K) g=5, h=0, h'=0 by terminate action (K means killed car)
S5: (V1, 0, 2, 1, 0, 2, F) g=0, h=2, h'=4 by moving to V1 (can still save people at V1)
S6: (V0, 1, 2, 0, 0, 2, F) g=0, h=3, h'=6 by moving to V0 (can no longer save anyone)
S7: (V3, 1, 0, 2, 0, 3, F) g=0, h=3, h'=6 by moving to V3 (can no longer save anyone)
Now pick S5 as it has the smallest f-cost f(S5)=0+2=2, and is is not a goal so:
RTA* returns it and the agent nakes the first move on this path, to A2.
A* expands S5 to get:
S8: (V1, 0, 2, 1, 0, 2, K1) g=6, h=0, h'=0 by terminate action (K1 means killed with 1 aboard)
S9: (V0, 0, 2, 0, 1, 5, F) g=0, h=2, h'=4 by moving to V1 (saved people from V1)
S10: (V2, 0, 2, 1, 0, 3, K1) g=6, h=0, h'=0 by moving to V2, missing the deadline, and getting killed
S11: (V3, 0, 0, 3, 0, 4, F) g=0, h=3, h'=6 by moving to V3 (can no longer save anyone)
A* now picks S9, the only state with f=2, and it is not a goal, to get:
S12: (V1, 0, 2, 1, 0, 8, F) g=0, h=2, h'=4 by moving to V1
S13: (V0, 0, 2, 0, 1, 5, T) g=2, h=0, h'=0 by terminate action
S14: (V2, 0, 2, 1, 0, 6, K) g=4, h=0, h'=0 by moving to V2, missing the deadline, and getting killed
Now A* actually has 2 states with f=2: S12, and S13. Supppose it prefers among equals to pick GOAL STATES,
wihich is a reasonable tie breaker. Then it picks S13 and terminates with the optimal path: move to V2,
then to V1, then to V0, then terminate, saving 1 preson which is optimal.
A* might pick S12, expand it to find the move to V3, which would make, among others, a state:
S15: (V3, 0, 0, 2, 1, 10, F) g=0, h=2, h'=6 by moving to V3 (already saved 1)
and may even cycle forever between V1 and V3 which have no deadlines, not recognizing that it is already dead...
How does this work with the theorem on optimality of A*? Well it IS optimal when it DOES terminate,
but here we have an infinite cycle with weight 0, with h-value unchanged, which makes A* not terminating possible.
Note, BTW that the heuristic defined in class has a simple bug that we should fix: need to add the
cost of the people in the vehicle (and vehicle itself) if it cannot reach a shelter before its deadline.
This modified heutistic H is still obviously admissible. With this fix, we will have H(S12)=4, and thus both A* and
RTA* will always pick S13 terminate the search optimally.
c) Continuing the RTA* algorithm, the agent moved to state S3, and expand it to get:
S4: (V2, 1, 2, 0, 0, 1, K) g=5, h=0, h'=0 by terminate action (K means killed car)
S5: (V1, 0, 2, 1, 0, 2, F) g=0, h=2, h'=4 by moving to V1 (can still save people at V1)
S6: (V0, 1, 2, 0, 0, 2, F) g=0, h=3, h'=6 by moving to V0 (can no longer save anyone)
S7: (V3, 1, 0, 2, 0, 3, F) g=0, h=3, h'=6 by moving to V3 (can no longer save anyone)
Now pick S5 as it has the smallest f-cost f(S5)=0+2=2, and is is not a goal so:
This time RTA* expand S5 to get:
S8: (V1, 0, 2, 1, 0, 2, K1) g=6, h=0, h'=0 by terminate action (K1 means killed with 1 aboard)
S9: (V0, 0, 2, 0, 1, 5, F) g=0, h=2, h'=4 by moving to V1 (saved people from V1)
S10: (V2, 0, 2, 1, 0, 3, K1) g=6, h=0, h'=0 by moving to V2, missing the deadline, and getting killed
S11: (V3, 0, 0, 3, 0, 4, F) g=0, h=3, h'=6 by moving to V3 (can no longer save anyone)
This is now 2 expansions so RTA* picks S9 and returns it, and the agent executes the first action, move to
V1, getting to state S5. RTA* now restarts from S5, to get:
S8: (V1, 0, 2, 1, 0, 2, K1) g=6, h=0, h'=0 by terminate action (K1 means killed with 1 aboard)
S9: (V0, 0, 2, 0, 1, 5, F) g=0, h=2, h'=4 by moving to V1 (saved people from V1)
S10: (V2, 0, 2, 1, 0, 3, K1) g=6, h=0, h'=0 by moving to V2, missing the deadline, and getting killed
S11: (V3, 0, 0, 3, 0, 4, F) g=0, h=3, h'=6 by moving to V3 (can no longer save anyone)
RTA* now picks S9, the only state with f=2, and it is not a goal, to get:
S12: (V1, 0, 2, 1, 0, 8, F) g=0, h=2, h'=4 by moving to V1
S13: (V0, 0, 2, 0, 1, 5, T) g=2, h=0, h'=0 by terminate action
S14: (V2, 0, 2, 1, 0, 6, K) g=4, h=0, h'=0 by moving to V2, missing the deadline, and getting killed
Again assuming preference for goal states, RTA* picks S13 and terminates. In this case agent actions in
RTA( and A* are the same.
d) Finally, using h'=2h. It makes no difference for greedy search in this example and in this domain, because g=0
except when h=h'=0, so there is no difference in node queue ordering.
For A* and RTA*, after expanding S0 we have f(S3)=4 and f(S1)=3, so now picks S1 which is a goal state,
so both would cause the terminate action, like the greedy search.
(In general multiplying the h by a factor
greater than 1 tends to make the seacrch "more greedy". Taking an admissible heuristic and multiplying it
by such a value is called "weighted A*", which may result in submoptimal paths, but usually the search runs faster.)
3) (Game trees 10%):
Consider a 3-person game (A, B, C) with complete information and STOCHASTIC environment.
Suppose A has 5 possible moves. Provide a game tree example that shows that for
each of the following set of "loyalties", A will have a different optimal move:
a) Each agent out for itself, and they cannot communicate (with ties broken anti-cooperatively).
b) B and C are semi cooperative (they break ties cooperatively)
c) B and C are partners aiming to maximize the sum of their scores
d) Paranoid assumption: B and C are against A
e) Even more paranoid assumption: B and C are against A, plus A is a firm believer in Murphy's
laws: "mother nature is a b*!=h", and believes the environment makes the worst thing for A always happen.
Explain your answer by showing the computed values in the internal nodes in each case.
Note that you should probably make the example more concise by allowing
only ONE choice of action for some of the players, or only ONE possible "stochastic" outcome
in some of the branches.
ANSWERS:
Consider the following tree (the score at the end is (A B C) scores, respectively).
A1 ----- B1 ---- C1 ----- (7 2 5)
C2 ----- (8 3 5)
B2 ---- C1 ----- (1 3 9)
C2 ----- (1 0 10)
A2 ----- B1 ---- C1 ----- chance 0.1 ----- (-4 2 5)
chance 0.9 ----- ( 6 2 5) ; expected scores: (5 2 5)
A3 ----- B1 ---- C1 ----- (0 2 5)
C2 ----- (0 1 2)
B2 ---- C1 ----- (9 9 9)
C2 ----- (4 0 10)
A4 ----- B1 ---- C1 ----- (2 20 0)
A5 ----- B1 ---- C1 ----- (6 2 5)
C2 ----- (0 1 2)
B2 ---- C1 ----- (4 3 9)
C2 ----- (9 2 10)
Note that in some of the cases B and/or C have only one possible move.
Under regime a, the best move for A is A1, because the optimal move for
B will be B1 and that for C will be C1 (C gets 5 in both cases, but prefers to give A and B less),
to get (7 2 5), i.e. a score of 7 for A.
This is the best A can get anywhere under this regime.
Under regime b, with ties broken cooperatively, the best move for A is A5 (same tree as A1 but numbers modified
to make B prefer a move that gives A a better score), as the play will be B2 and C2.
Under regime c, the best move for A is A3, as B and C will shoot for (9 9 9), i.e. 18 together,
thus giving A 9.
Under regime d, the best move for A is A2, which gives B and C no options, and results in 5 for A, in expectation.
Any other choice allows B and C together to make A get less than 5.
Finally, under regime e, the best move for A is A4: as A will always get 2, whereas for every other move
it is possible for A to get less. Because everybody (including chance) is assumed to be against A,
every possible bad thing is "guaranteed to happen".
4) (Game-tree search - alpha-beta pruning - 15%)
In the adversarial version of the hurricane evacuation problem:
a) Construct an example where the optimal first move is no-op (assuming such an action is allowed),
or argue that this cannot be the case.
b) Construct and show an example (including the static heuristic evaluation function and
search tree), with a tree depth of at least 4 ply.
c) Show where alpha-beta pruning can decrease search effort in the tree from b.
ANSWER:
a) Assume no-op does nothing except consume 1 time unit. We have agents A and B, with A moving first
in every time unit. Consider the following graph with 6 nodes:
VA, VB (also initial location for respective agent)
P1, P2, Pe with the first 2 containing 5 people each and Pe containing 1
Node S contains a shelter, and has a deadline of 8, with all other vertices having a deadline of 10.
The edges are:
(VA, P1) and (VA, P2) with weight 5
(VB, P1) and (VB, P2) with weight 4
(P1, S) and (P2, S) with weight 2
(Pe, S) with weight 1
This is set up so that, left to themselves, player A can collect and save people at either P1 or P2, but not both, and also
at Pe, saving 6 people total, but only if A starts to move immeditely.
Player B can collect and save people at either P1 or P2, but not both, and also at Pe, and can afford to weight 1 unit.
However, if A starts moving towards P1, then B will start moving towards P1 as well and thus A will lose by 6, as B
will arrive at P1 and at Pe before A, and A cannot change and move to P2.
However, if A does a no-op to see how B moves, it can improve its score.
Now if B moves towards P1, A can move towards P2 and thus will be able to collect
and save the 5 people at P2 and lose only by 1. So B should also wait by doing no-op: by doing that, it no longer
can collect the people at Pe but makes sure that A cannot collect anyone.
In the second turn, A still cannot move without losing 5, and no-op also loses 5, so A loses by 5 (B can no longer
collect and save people at Pe).
By doing no-op in the first turn, A loses only 5 instead of 6 (any other move), so no-op is optimal for A.
By doing no-op in the first turn, B forces A to lose by 5, instead of only by 1 (any other move), so no-op is optimal for B as well.
b) Here we will set up the following graph, with nodes VA, VB (initial agnt locations), P1, P2, V, S, and the
following edges, all with weight 1: (VA, P1), (VA, P2), (VB, P2), (VB, V), (P1, S), (P2, S), (V, S)
with 1 person each at P1 and P2, shelter at S (all nodes with deadline 2).
Assuming only traversals and terminate are possible (no "no-ops"), we have the following 4-ply tree (assuming cutoff at 4 ply).
In the tree we denote moves by AGENT, Move to VERTEX with T denoting "terminate", X denoting "already terminated", followed by a number
denoting the score of the node: heuristic or terminal value, or value comupted by minimax for internal nodes.
Nodes pruned by alpha-beta assuming order of expansion according to the order of lines from top to bottom are indicated by "pruned".
Correct move for A initially is to P2, to grab 1 person and stealing from B.
AP2 1 ---- BV 1 ---- AS 1 ---- BS cutoff, h=1 (A has saved 1, B cannot save any)
---- BT cutoff, h=3 (A has saved 1, B is dead)
---- BVB cutoff, h=1 (A has saved 1, B is doomed but heuristic does not know it)
---- AVA 0 ---- BS cutoff, h=0 (nothing can be saved, A is doomed but heuristic does not know it)
---- BT cutoff, h=2 pruned, as A will not pick the branch AVA
---- BVB cutoff, h=0 pruned (same)
---- AVB 0 (same as subtree for AVA, omitted)
---- AT -3 ---- BS cutoff, h=-3 (A is dead with 1 aboard)
---- BT cutoff, h=-1 pruned
---- BVB cutoff, h=-3 pruned
BP2 1 ---- (similar to above subtree for BV due to symmetry, 1 additional useless branch BVA for B)
BT 3 ---- AS 3 ---- BX 3 cutoff, h=3 (A has saved 1, B is dead)
AVA 2 ---- BX 2 cutoff, h=2 (A cannot save anyone, B is dead) pruned, B will not take this the branch BT
AVB 2 ---- BX 2 cutoff, h=2 (A cannot save anyone, B is dead) pruned
AT -1 ---- terminal, value -1 (A is dead with 1 aboard, B is dead)
AP1 0 ---- BP2 0 ---- AS 0 ---- BS cutoff, h=0 (A has saved 1, B has saved 1)
---- BT cutoff, h=4 (A has saved 1, B is dead with 1 aboard)
---- BVB cutoff, h=1 (A has saved 1, B is doomed but heuristic does not know it)
---- AVA -1 ---- BS cutoff, h=-1 (B saved 1, A is doomed but heuristic does not know it)
---- BT cutoff, h=1 pruned, as A will not pick the branch AVA
---- BVB cutoff, h=0 pruned (same)
---- AT -3 ---- BS cutoff, h=-4 (A is dead with 1 aboard, B saved 1)
---- BT cutoff, h=0 pruned
---- BVB cutoff, h=-3 pruned
BV 1 ---- (similar to above subtree under AP2 for BV due to symmetry)
BT 3 ---- AS 3 ---- BX 3 cutoff, h=3 (A has saved 1, B is dead)
AVA 2 ---- BX 2 cutoff, h=2 (A cannot save anyone, B is dead) pruned, B will not take this the branch BT
AVB 2 ---- BX 2 cutoff, h=2 (A cannot save anyone, B is dead) pruned
AT -1 ---- terminal, value -1 (A is dead with 1 aboard, B is dead)
AT -3 ---- BP2 -3 --- AX -3 ---- BS cutoff, h=-3 (B has saved 1, A is dead)
---- BT terminal, h=1 (both dead, B with 1 aboard) pruned
---- BVB cutoff, h=-2 pruned
BV -2 --- AX -2 ---- BS cutoff, h=-2 (B can save nobody, A is dead) pruned
---- BT terminal, h=0 (both dead), pruned
---- BVB cutoff, h=-2 pruned
BT 0 terminal, both A and B are dead. pruned
5) (Propositional logic - 10%)
For each of the following sentences, determine whether they are
satisfiable, unsatisfiable, and/or valid. For each sentence
determine the number of models (over the propositional
variables in the sentence).
Note: some items seem hard, but if you use some (natural) intelligence, easier than it may seem.
a) (not A and not B and not C and not D and not E and F) or (A and B and C and D and E)
b) (A or B or C or D or E or F) and (not A or not B or not C or not D or not E or not F)
c) (A or B and (D or not A) and (E or A) -> (B or C and (not D or E))) and (A and not A)
d) (A and (A -> B) and (B -> C)) -> C
e) not ((A and (A -> B) and (B -> C)) -> C)
f) (A -> not A) or (not A -> A)
Bonus question: in cases a, b, c, also trace the run of the DPLL algorithm
for satisfiability with this formula as input (i.e. explain any recursive calls and
cases encountered).
ANSWERS:
a) Satisfiable, 3 models: (A through E false and F true), (A through E true) with F either true or false.
b) Satisfiable, 2^6-2=62 models: all assignments except either all propositions true or all propositions false.
c) Unsatisfiable, because we have a conjunction with the unsatisfiable (A and not A)
d) Valid (2^3=8 models), because B is entailed by (A and A->B) and C is entailed by (B and B->C)
e) Unsatisfiable, because this is a negation of a valid sentence.
f) Strangely enough, this sentence is VALID (2 models).
6) (FOL and situation calculus - 40%)
We need to represent and reason within the scenario defined by assignment 1.
For simplicity, we will assume only one agent.
a) Write down the axioms for the behavior of the world using FOL and
situation calculus.
Use the predicates:
Vertex(v) ; v is a vertex
Edge(e, v1, v2) ; e is an edge in the graph between v1 and v2
Shelter(v) ; Vertex v is contains a Hurricane shelter
Weight(e,w) ; Weight of edge e is w
Deadline(v,t) ; The deadline for vertex v is at time t
Also use the fluents (situation-dependent predicates)
Loc(v,s) ; Agent is at vertex v in situation s
Carrying(n,s) ; Agent is carrying n people in situation s.
Safe(n,s) ; In situation s, n people are safe
At(v,n,s) ; There are n people at vertext v in situation s
Time(t,s) ; The time since creation is t in situation s
Constants: as needed, for the edges and vertices, and simple actions (terminate).
Functions:
traverse(e) ; Denotes a traverse move action across edge e
and of course the "Result" function:
Result(a,s) ; Denotes the situation resulting from doing action a in
; situation s.
You may wish to add auxiliary predicates or fluents in order to simplify the axioms.
You are allowed to do so provided you explain why they are needed.
Let the facts representing the scenario be:
Edge(E1, V0, V1)
Edge(E2, V0, V2)
Edge(E3, V2, V3)
Edge(E4, V1, V3)
Edge(E5, V1, V2)
Weight(E1,3)
Weight(E2,1)
Weight(E3,2)
Weight(E4,2)
Weight(E5,1)
Deadline(V2,2)
Deadline(V0,5)
Shelter(V0)
; with situation S0 fluents being (note that this is a partial, "closed world assumption" description).
Loc(V0, S0)
Carrying(0, S0)
At(V1, 1, S0)
At(V3, 2, S0)
Safe(0, S0)
Time(0, S0)
b) Now, we need to find a sequence of actions that will result some people
being safe, starting from S0 (which you found in question 1 above),
and prove a theorem that some (not zero) people are safe as a result
(but do not need to prove optimality). Do this by the following steps:
A) Convert the knowledge base into conjunctive normal form. (This is very long,
so you may omit the parts not needed in the proof below).
B) Formally list what we need to prove (a theorem), and state its negation.
C) Use resolution to reach a contradiction, thus proving the theorem.
At each step of the proof, specify the resolvents and the unifier.
For simplicity, you may (recommended!) omit the time keeping and the deadline requirements for
action success from the KB before doing the proof. (Say exactly which axioms you are
changing in order to do that, if you decide to simplify).
c) Would there be a potential problem in the proof if we did not
have "frame axioms" in our representation (i.e. stating what
did not change), and if so, what?
d) Would we be able to do the proof using only forward chaining?
ANSWERS:
We will begin by adding some auxiliary predicates and fluents. First, we will have a predicate indicating
whether a vertex v had people originally, call it PO(v), and we add to the simple facts in the KB:
PO(V1)
not PO(V2)
PO(V3)
not PO(V4)
not PO(V5)
Note how we are applying the closed-world assumption, adding the vertices with NO people mentioned
and assuming explicitly that if none were stated it means that none were there.
Also needed are the foolish-looking "obvious" (to a human, not to the AI!) axioms like:
not V1=V2
not V0=V2
not E1=E2
etc. Note that we wish in general to avoid using equality, but here we have to do so,
and we will use equality in a very limited way which will not lead to trouble.
We need some predicates for handling numbers. +(a, b, sum) will be true if sum is the sum of a and b,
and Leq(a, b) will be true if a is less than or equal to b.
We need a sucessor function S(a) indicating the integer successor of a.
Note that these are not complete axiomatizations, for integers we need to say that "not a=S(a)" etc. but
we will not need these axioms in our proof. We then can give names to the numbers, by using the following as
shorthand. That is, replace the strings by the appropriate long notation in the KB before doing the reasoning:
1 = S(0)
2 = S(S(0))
etc.
We need to axiomatize addition, which we can do by:
Forall x, +(x, 0, x) and +(0, x, x)
Forall x, y, z, +(x, y, z) -> (+(x, S(y), S(z)) and +(S(x), y, S(z))
We also need to axiomatize Leq:
Forall x, Leq(x, x) and Leq(x, S(x))
Forall x, y, z, (Leq(x,y) and Leq(y,z)) -> Leq(x,z)
In the proof we will take a shortcut, assuming the KB already contains all relevant
such sentences, such as "Leq(2,4)", and "+(2,2,4)".
We will add a fluent OK(action, source, destination, s) to indicate that an action proceeds "normally" if done
in situation s, i.e. makes sense starting from vertex "source" to vertex "destination" (if relevant), and does not violate a deadline.
If there is an edge from v1 to v2, the time now is t, less than the deadline at v1,
the agent is at v1, the weight of e is w, and the deadline at v2 is Leq p (the sum of t and w), then traversing e is OK:
Forall v1, v2, e, s, t, d1, d2, p, (Edge(e, v1, v2) and Time(t,s) and Loc(v1,s) and Weight(e, w) and Deadline(v1, t1) and Leq(t, d1)
Deadline(v2, d2) and +(t, w, p) and Leq(p, d2)) -> OK(traverse(e), v1, v2, s)
Using the OK fluent we can now define effects of traversal. We start with updating the clock:
Forall s, e, v1, v2, t1, t2, w, (Time(t1,s) and Weight(e,w) and OK(traverse(e), v1, v2, s) and +(t1, w, t2)) ->
Time(t2,Result(traverse(e), s))
Now updating the location:
Forall s, e, v1, v2, OK(traverse(e), v1, v2, s) -> Loc(v2,Result(traverse(e), s))
Updating the Carrying and At fluents for pickup:
Forall s, e, v1, v2, po, pn, pp, (OK(traverse(e), v1, v2, s) and Carrying(po, s) and At(v2,pp,s) and +(po, pp, pn)) ->
Carrying(pn,Result(traverse(e), s)) and At(v2, 0, Result(traverse(e), s))
Updating the Safe and Carrying fluents at shelter (assuming no people at shelter originally!):
Forall s, e, v1, v2, po, pn, pp, (OK(traverse(e), v1, v2, s) and Shelter(v2) and Safe(po, s) and Carrying(pp,s) and +(po, pp, pn)) ->
Safe(pn,Result(traverse(e), s)) and Carrying(0, Result(traverse(e), s))
We will also need to prove zero people at nodes which never had any, we can use the PO predicate and need the followin axiom:
Forall v, s, not PO(v) -> At(v, 0, s)
We need to state that edges are undirected by a symmetry axiom:
Forall e, v1, v2, Edge(e, v1, v2) -> Edge(e, v2, v1)
This seems OK for now, except that we "forgot" frame axioms. We will return to them later (the above saves at one
type of frame axiom, but others needed).
b) Proof using the KB
A) Converting to CNF:
Forall v1, v2, e, s, t, d1, d2, p, (Edge(e, v1, v2) and Time(t,s) and Loc(v1,s) and Weight(e, w) and Deadline(v1, t1) and Leq(t, d1)
Deadline(v2, d2) and +(t, w, p) and Leq(p, d2)) -> OK(traverse(e), v1, v2, s)
After eliminating the implication, De-Morgan to move in negation, and removing the universal quantifiers, becomes:
1. not (Edge(e, v1, v2) or not Time(t,s) or not Loc(v1,s) or not Weight(e, w) or not Deadline(v1, t) or not Leq(t, d1)
or not Deadline(v2, d2) or not +(t, w, p) or not Leq(p, d2) or OK(traverse(e), v1, v2, s)
Forall s, e, v1, v2, t1, t2, w, (Time(t1,s) and Weight(e,w) and OK(traverse(e), v1, v2, s) and +(t1, w, t2)) ->
Time(t2,Result(traverse(e), s))
Similar operations as above, we get:
2. not Time(t1,s) or not Weight(e,w) or not OK(traverse(e), v1, v2, s) or not +(t1, w, t2) or Time(t2,Result(traverse(e), s))
Forall s, e, v1, v2, OK(traverse(e), v1, v2, s) -> Loc(v2,Result(traverse(e), s))
In CNF we have:
3. not OK(traverse(e), v1, v2, s) or Loc(v2,Result(traverse(e), s))
Forall s, e, v1, v2, po, pn, pp, (OK(traverse(e), v1, v2, s) and Carrying(po, s) and At(v2,pp,s) and +(po, pp, pn)) ->
Carrying(pn,Result(traverse(e), s)) and At(v2, 0, Result(traverse(e), s))
Due to the conjunction on the RHS, this will distribute into two clauses:
4.1 not OK(traverse(e), v1, v2, s) or not Carrying(po, s) or not At(v2,pp,s) or not +(po, pp, pn) or Carrying(pn,Result(traverse(e), s))
4.2 not OK(traverse(e), v1, v2, s) or not Carrying(po, s) or not At(v2,pp,s) or not +(po, pp, pn) or At(v2, 0, Result(traverse(e), s))
Forall s, e, v1, v2, po, pn, pp, (OK(traverse(e), v1, v2, s) and Shelter(v2) and Safe(po, s) and Carrying(pp,s) and +(po, pp, pn)) ->
Safe(pn,Result(traverse(e), s)) and Carrying(0, Result(traverse(e), s))
Also becomes two clauses:
5.1 not OK(traverse(e), v1, v2, s) or not Shelter(v2) or not Safe(po, s) or not Carrying(pp,s) or not +(po, pp, pn)) or Safe(pn,Result(traverse(e), s))
5.2 not OK(traverse(e), v1, v2, s) or not Shelter(v2) or not Safe(po, s) or not Carrying(pp,s) or not +(po,pp,pn)) or Carrying(0,Result(traverse(e),s))
Forall v, s, not PO(v) -> At(v, 0, s)
becomes:
6. PO(v) or At(v, 0, s)
Forall e, v1, v2, Edge(e, v1, v2) -> Edge(e, v2, v1)
becomes:
7. not Edge(e, v1, v2) or Edge(e, v2, v1)
The basic graph and initial state description are already CNF clauses, as are the "explicit" number axioms,
so we will not number them but use them as needed in the proof.
B) Stating what we need to prove. We know that traversing E2 to V2, then E5 to V1, then E1 to V0 is supposed to save some people.
To formally prove that some (at least 1) people are safe as a result we need to prove:
Q. Exists n, Leq(1,n) and Safe(n, Result(traverse(E1), Result(traverse(E5), Result(traverse(E2), S0))))
The negation is:
not Exists n, Leq(1,n) and Safe(n, Result(traverse(E1), Result(traverse(E5), Result(traverse(E2), S0))))
In CNF this becomes:
Q'. not Leq(1, n) or not Safe(n, Result(traverse(E1), Result(traverse(E5), Result(traverse(E2), S0))))
C) Resolution proof will proceed as follows. For each action, we will first show that it is OK in its respective
situation, then use that to show some or all properties of the situation resulting from the action, and repeat until
we can prove the Safe property of the third and last action. We will take some shortcuts for conciseness
in cases of similar steps, which we will indicate below. There is more than one way to do the proof.
Resolve 1. with "Edge(E2, V0, V2)", unifier {e/E2, v1/V0, v2/V2} to get:
100. not Time(t,s) or not Loc(V0,s) or not Weight(E2, w) or not Deadline(V0, t) or not Leq(t, d1)
or not Deadline(V2, d2) or not +(t, w, p) or not Leq(p, d2) or OK(traverse(E2), V0, V2, s)
Resolve 100 with "Time(0, S0)", unifier {t/0, s/S0} to get:
101. not Loc(V0,S0) or not Weight(E2, w) or not Deadline(V0, t) or not Leq(t, d1)
or not Deadline(V2, d2) or not +(t, w, p) or not Leq(p, d2) or OK(traverse(E2), V0, V2, S0)
Resolve 101 with "Loc(V0,S0)", empty unifier, to get:
102. not Weight(E2, w) or not Deadline(V0, t) or not Leq(t, d1)
or not Deadline(V2, d2) or not +(0, w, p) or not Leq(p, d2) or OK(traverse(E2), V0, V2, S0)
Resolve 102 with "Weight(E2,1)", unifier {w/1} to get:
103. not Deadline(V0, d1) or not Leq(0, d1) or not Deadline(V2, d2) or not +(0, 1, p) or not Leq(p, d2) or OK(traverse(E2), V0, V2, S0)
Resolve 103 with "Deadline(V0, 5)", unifier {d1/5} to get:
104. not Leq(0, 5) or not Deadline(V2, d2) or not +(0, 1, p) or not Leq(p, d2) or OK(traverse(E2), V0, V2, S0)
Resolve 104 with Leq axiom "Leq(0, 5)", empty unifier, to get:
105. not Deadline(V2, d2) or not +(0, 1, p) or not Leq(p, d2) or OK(traverse(E2), V0, V2, S0)
Resolve 105 with "Deadline(V2, 2)", unifier {d2/2}, to get:
106. not +(0, 1, p) or not Leq(p, 2) or OK(traverse(E2), V0, V2, S0)
Resolve 106 with arithmetic axiom "+(0, x, x)", unifier {x/1, p/1} to get:
107. not Leq(1, 2) or OK(traverse(E2), V0, V2, S0)
Now resolve 107 with Leq axiom "Leq(1,2)" to finally get:
108. OK(traverse(E2), V0, V2, S0)
With this in hand, we can now prove things about the situation resulting from the execution of traversing E2 in S0, starting with time.
Resolve 108 with 2, unifier {e/E2, v1/V0, V2/V2, s/S0} to get:
110. not Time(t1,S0) or not Weight(E2,w) or not +(t1, w, t2) or Time(t2,Result(traverse(E2), S0))
Resolve 110 with "Time(0, S0)", unifier {t1/0} to get:
111. not Weight(E2,w) or not +(0, w, t2) or Time(t2,Result(traverse(E2), S0))
Resolve 111 with "Weight(E2,1)", unifier {w/1} to get:
112. not +(0, 1, t2) or Time(t2,Result(traverse(E2), S0))
Resolve 112 with arithmetic axiom "+(0, x, x)", unifier {x/1, t2/1} to get:
113. Time(1,Result(traverse(E2), S0))
Now the location, resolve 108 with 3, unifier {e/E2, v1/V0, V2/V2, s/S0} to get:
114. Loc(V2,Result(traverse(E2), S0))
Now the Carrying fluent, resolve 4.1 with 108, unifier {e/E2, v1/V0, V2/V2, s/S0} to get:
115. not Carrying(po, S0) or not At(V2,pp,S0) or not +(po, pp, pn) or Carrying(pn,Result(traverse(E2), S0))
Resolve 115 with "Carrying(0, S0)", unifier {po/0} to get:
115. not At(V2,pp,S0) or not +(0, pp, pn) or Carrying(pn,Result(traverse(E2), S0))
Resolve 6 with "not PO(V2)", unifier {v/V2} to get:
116. At(V2,0,s)
Resolve 116 with 115, unifier {pp/0, s/S0} to get:
117. not +(0, 0, pn) or Carrying(pn,Result(traverse(E2), S0))
Resolve 117 with arithmetic axiom "+(0, x, x)" unifier {x/0, pn/0} to get:
118. Carrying(0,Result(traverse(E2), S0))
So now we SEEM to have what we need to proceed to handline the 2nd action, but first must prove the edge from V2 to V1:
Resolve "Edge(E5,V1,V2)" with 7, unifier {e/E5, v1/V1, v2/V2} to get:
119. Edge(E5,V2,V1)
And now we can proceed with the 9 steps to prove that the 2nd action is OK, similar to the steps (100 through 108)
done for the 1st action. Here we take a short cut by just describing the steps. (Do NOT do such shortcuts in the midterm exam!!!)
Start again by resolving 1 with 119: Edge(E5,V2,V1), and the result with 113: Time(1,Result(traverse(E2), S0)), and
then with 114: Loc(V2,Result(traverse(E2), S0)), then with "Weight(E5,1)", then with Deadline(V2,2),
then with "Leq(1, 2)", and then with... Deadline(V1, d)... No such thing in the KB!!!
OOPS, we are STUCK. We MUST have in the KB something there, or we cannot prove that the move is OK! Suppose the KB
DID contain "Deadline(V1, 10)". Now we can continue resolving with the latter sentence.
Now resolve the result with "+(1, 1, 2)" and then the result with "Leq(2,10)" finally getting:
130. OK(traverse(E5), V2, V1, Result(traverse(E2), S0))
Now we take the steps to prove properties of the situation: Result(traverse(E5), Result(traverse(E2), S0)), and again do a shortcut
as the steps are similar to steps 100 through 113. Resolving 2 with 130, then the result with 113, then with "Weight(E2,2)", then
with "+(1,1,2)" we get:
140. Time(2, Result(traverse(E5), Result(traverse(E2), S0)))
Resolving 130 with 3, we get:
141. Loc(V1, Result(traverse(E5), Result(traverse(E2), S0)))
Now similar to steps 115 through 118, we resolve 4.1 with 130, then the result with 118, to get:
142. not At(V1,pp,Result(traverse(E2), S0)) or not +(0, pp, pn) or Carrying(pn,Result(traverse(E5), Result(traverse(E2), S0)))
Now we need to resolve 142 with "At(V1,1,?)" ???
Ooops again, we have a problem. We have "At(V1,1,S0)" but we do NOT have "At(V1,1,Result(traverse(E2), S0))", and CANNOT
prove it, either! We are missing a FRAME AXIOM that means that fluent stays constant unless the agent enters node V1!
We avoided this issue for "At(V2,0,s)" because we had that no people initially implies NEVER any people, but for V1
this cannot be done. Assuming the only action is traverse(e), we need a frame aviom stating that if the traversal is to
a DIFFERENT node, that value of the At stays the same. That is:
Forall e, v, v1, v2, s, n, Loc(v1, s) and Edge(e, v1, v2) and At(v, n, s) and not v=v2 -> At(v,n,Result(traverse(e), s))
In CNF we wouid have had this axiom as the frame axiom:
F1. not Loc(v1, s) or not Edge(e, v1, v2) or not At(v, n, s) or v=v2 or At(v,n,Result(traverse(e), s))
Now we can proceed with the proof. Resolve F1 with "Loc(V0,S0)", unifier {v1/V0, s/S0} to get:
150. not Edge(e, V0, v2) or not At(v, n, S0) or v=v2 or At(v,n,Result(traverse(e), S0))
Resolve 150 with "Edge(E2,V0,V2)", unifier {e/E2, v2/V2} to get:
151. not At(v, n, S0) or v=V2 or At(v,n,Result(traverse(E2), S0))
Resolve 151 with "At(V1,1,S0)", unifier {v/V1, n/1} to get:
152. v=V2 or At(v,n,Result(traverse(E2), S0)
Now resolve 152 with "not V1=V2", unifier {v/V1} to get:
153. At(V1,1,Result(traverse(E2), S0))
And only NOW we can continue to resolve 142 with 153, unifier {pp/1} to get:
154. not +(0, 1, pn) or Carrying(pn,Result(traverse(E5), Result(traverse(E2), S0)))
And finally resolve 154 with "+(0, x, x)", unifier {x/1, pn/1} to get:
155. Carrying(1,Result(traverse(E5), Result(traverse(E2), S0)))
Now we proceed to prove that traverse(E1) is OK in Result(traverse(E5), Result(traverse(E2), S0)), where again we
will just mention the steps. Resolve 1 with "Edge(E1, V1, V0)" (assuming it is already in the KB, and if not derive it
using "Edge(E1,V0,V1)" and the edge symmetry axiom), then with time axiom 140 to get Time 2, then with 141 to get location V1,
then with "Weight(E1,3)" to get the weight 3, then with "Deadline(V1,10)", then with "Leq(2,10)", then with "Deadline(V0,5)",
then with "+(2, 3, 5)", them with "Leq(x,x)" to get:
160. OK(traverse(E1), V1, V0, Result(traverse(E5), Result(traverse(E2), S0)))
For conciseness, we will denote S2=Result(traverse(E5), Result(traverse(E2), S0)), as a PRESENTATION CONVENIENCE.
Now we finally get to proving safety... Resolve 160 with 5.1, unifier {e/E1, v1/V1, v2/V0, s/S2} to get:
161. not Shelter(V0) or not Safe(po, S2) or not Carrying(pp,S2) or not +(po, pp, pn)) or Safe(pn,Result(traverse(e), S2))
Resolve 161 with "Shelter(V0)" to get:
162. not Safe(po, S2) or not Carrying(pp,S2) or not +(po, pp, pn)) or Safe(pn,Result(traverse(e), S2))
We can now resolve 162 with 155 (recall that S2 is actually "Result(....)", unifier {pp/1} to get:
163. not Safe(po, S2) not +(po, 1, pn)) or Safe(pn,Result(traverse(e), S2))
But now we are STUCK again, because we DO have "Safe(0, S0)" but we CANNOT PROVE "Safe(n, s)" for any other situation!
AGAIN missing a frame axiom, that the Safe fluent is not changed unless moving into a shelter! Need a frame axiom like:
Forall n, s, v1, v2, Loc(v1, s) and Edge(e, v1, v2) and not Shelter(v2) and Safe(n,s) -> Safe(n, Result(traverse(e),s))
or in CNF, we have:
F2. not Loc(v1, s) or not Edge(e, v1, v2) or Shelter(v2) or not Safe(n,s) or Safe(n, Result(traverse(e),s))
Now we can use F2, resolve it with "Loc(V0,S0)", and the result with "Edge(E2,V0,V2)" and then with "not Shelter(V2)"
(note the need for the "closed world assumption" here: no shelter anywhere unless specified!), then with "Safe(0, S0)" to get:
170. Safe(0, Result(traverse(E2),S0))
Now we need to continue in a similar manner, to get:
180. Safe(0, S2)
And NOW we can finally take the last few steps to complete the proof:
Resolve 180 with 163, unifier {po/0} to get:
181. not +(0, 1, pn)) or Safe(pn,Result(traverse(E1), S2))
Resolve 181 with "+(0,x,x)", unifier {x/1, pn/1} to get:
182. Safe(1,Result(traverse(E1), S2))
Then resolve 181 with Q', unifier {n/1} (recall what S2 stands for), to get:
183. not Leq(1, 1)
And, FINALLY, resolve 183 with "Leq(x,x)", unifier {x/1} to get the empty clause, proof by contradiction is complete!
c) We saw above that we could NOT complete the proof without frame axioms for "At" and for "Safe". We added them above
during the proof, but of course such axioms must be in the KB ab-initio.
d) We used some axioms that were NOT in Horn form (e.g. axiom 6: "PO(v) or At(v,0,s)", which has 2 positive literels),
and as the KB was stated there is no way around them, so cannot do the proof using just Generalized modus ponens
and therefore cannot be done by backward or forward chaning.
There MAY be ALTERNATE ways to write the KB to avoid such clauses, such as replacing axiom 6 by an appropriate frame axiom,
or defining new special predicates, etc. but the answer to this question as the KB was written is NO.
Deadline: (16:00), Tuesday, December 10, 2019 ( strict deadline).
Submissions are to be solo.