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) An agent that can play Soduko (easy), and Sudoku (hard).
c) An autonomous humanoid robot that can win the DARPA robotics challenge (driving a car,
walking across debris, connecting two pipes). Scoring depends on success in the tasks,
on execution speed, and on using as little communication with the operator as possible.
d) An internet shopping agent specializing in cheap flights.
e) An agent that can play Go.
ANSWER:
a) Utility based agent, since you are trying to get as much money (utility) as possible.
Environment is discrete, stochastic, partially observable, non-episodic, (semi) static, multi-agent
b) Can use a reflex agent for easy Sudoku.
Really hard instances require backtracking search, i.e. a goal-based agent.
Environment is discrete, deterministic, fully observable, episodic, static, single-agent.
c) Utility based agent. Also probably needs learning. Environment is continuous, stochastic,
partially observable, non-episodic, dynamic, and some of the tasks are multi-agent.
d) Utility-based agent. Environment is continuous (but can be modeled as discrete),
stochastic, partially observable, non-episodic, dynamic, multi-agent.
e) Goal-based or utility-based agent. Environment is discrete, deterministic, fully observable,
non-episodic, static, and multi-agent.
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 reach the goal vertex G with minimal cost,
where costs are as defined in assignment 1.
Assume that h(n) is the cost to reach the goal state in the simplified problem
that assumes that the agent gets all the keys for free.
a) Greedy search (f(n) = h(n)), breaking ties in favor of states where the
higher node number.
ANSWER:
Essential elements of a state are agent location, has the key been picked, and whether the lock
still exists. We will thus use tuples (loc, has-key, locked) to denote the state, in all answers here.
In all cases, initialize and push initial state:
S0: (V0, F, T) with h=2, g=0, f=2
Now start the seach loop. Retrieve S0, not a goal, and only one legal successor (we ignore noops,
which are useless and give us repeated states anyway, which we assume are discarded), and it
is now the only item in the agenda:
S1: (V1, T, T) with h=3, g=1, f=4
Now get S1, which is not a goal, so expand to get:
S2: (G, T, T) with h=0, g=5, f=5
S3: (V0, T, T) with h=2, g=2, f=4
In greedy search we pick S2, since h(S2)=0, it is a goal, so we terminate,
returning the path "go to V1, then V4" for a cost of 5.
b) A* search, (f(n) = g(n)+h(n)), breaking ties as above.
ANSWER:
Starts the same as greedy, except at the last step picks S3 since f(S3)=4 which is
lower then f(S2). It is not a goal, so expands it to get (removing duplicates)
S4: (V2, F, F) with h=1, g=3, f=4
Now S4 is also preferred to S2, so picks S4. Not a goal, so expands and adds:
S5: (G, F, F) with h=0, g=4, f=4
S6: (V0, F, F) with h=2, g=4, f=6
Now S6 is best, so pick it, and it is a goal state so return it, and
the path implied is: "Go to V1, then V0, then V2, then G" for a cost of 4.
c) Simplified RTA* with a limit of 2 expansions per real action, breaking ties as above.
ANSWER:
First 2 expansions as in previous cases. Now stop and do the first action: "Go to V1".
Now re-start the search from state S1, so we have:
S1: (V1, T, F) with h=3, g=0, f=3
Pick it and not a goal, so expand and get:
S2: (V0, T, F) with h=2, g=1, f=3
S3: (G, T, F) with h=0, g=4, f=4
Now pick S2, not a goal but limit reached, so do action "go to V0" and re-start the search from S2.
Pick it and expand it, to get:
S4: (V1, T, F) with h=3, g=1, f=4 (note that S4 is the same as S1, but we do not detect duplicates
as this is a new search).
S5: (V2, F, F) with h=2, g=1, f=3
Now pick S5, not a goal, and expand it, to get:
S6: (V0, F, F) with h=2, g=2, f=4
S7: (G, T, F) with h=0, g=2, f=2
Now pick S7, limit but it is a goal so return it, and can now do actions "go to V2, go to G"
ending up in the same actions as in A*. Overall search time needed is higher, but the maximum
computation time per step is lower than A*.
d) Repeat a-c but using h'(n) = 2*h(n) as the heuristic. Is h'(n) admissible?
ANSWER:
Greedy uses h'(n)=2*h(n) as the node ordering, which is a linear multiple so does not
affect the run at all (except that the h values are doubled).
In A* we start the same as greedy for the first 2 steps, and now get:
S2: (G, T, T) with h'=0, g=5, f=5
S3: (V0, T, T) with h'=4, g=2, f=6
This time we pick S2, and it is a goal, so we are done. So we get a behaviour same
as greedy due to the (obviously inadmissible) heuristic h'. Note that this is shown by the fact
that the result was not the optimal path, but also seen by example, since we had h'(S3)=4 whereas
in fact we can reach the goal there for a cost of 2.
Note that RTA* would behave exactly like A*, because A* only did 2 expansions.
3) (Game trees 10%):
Consider a 4-person game (A, B, C, D) with complete information and deterministic environment.
Suppose A has 5 possible moves. Provide a game tree example that shows that for
each of the following set of rules, A will have a different optimal move:
a) Each agent out for itself, and they cannot communicate.
b) Paranoid assumption: B and C are against A
c) B and C may agree on a deal if it is beneficial to both of them
d) A and C are partners aiming to maximize the sum of their scores
e) A and B may reach a deal, if it is beneficial to both of them
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 in some of the branches.
ANSWER:
Consider the following tree (the score at the end is (A B C D) scores, respectively).
A1 ----- B1 ---- C1--D1----- (7 2 5 0)
C2--D1----- (0 1 2 0)
B2 ---- C1--D1----- (4 3 9 0)
C2--D1----- (4 0 10 0)
B3 ---- C1--D1----- (4 2 5 0)
A2 ----- B1 ---- C1--D1----- (2 2 5 0)
C2--D1----- (0 0 2 0)
C3--D1----- (9 0 4 0)
B2 ---- C1--D1----- (4 3 9 0)
C2--D1----- (5 0 10 0)
C3--D1----- (8 0 8 0)
A3 ----- B1 ---- C1--D1----- (6 1 0 0)
B3 ---- C1--D1----- (4 0 0 0)
A4 ----- B1 ---- C1--D1----- (9 5 0 0)
B2 ---- C1--D1----- (0 10 0 0)
A5 ----- B1 ---- C1--D1----- (5 0 0 0)
Note that in some of the cases B and/or C and/or D 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, to get (7 2 5 0), i.e. a score of 7 for A. D has no
choice, so is irrelevant.
This is the best A can get anywhere under this regime.
Under regime b, the best move for A is A5, which gives B and C no options, and results in 5 for A.
Any other choice allows B and C together to make A get less than 5.
Under regime c, if A takes move A1 (or A2) then B and C can make a deal that will benefit both:
B will agree to make move B2 if C agrees to move to C1, improving the score for both B and C.
As a result the score starting at A1 is (4 3 9 0), so A will only get 4, and as a result
the best move for A is A3 which earns 6 for A.
(Doing A2 will cause the deal between B and C to be (4 3 9 0) which is also not good for A.
Under regime d, A can play A2, requesting C to take option 3, and, depending on what B does,
give A 8 or 9 and C 4 or 8. Otherwise, A threatens to play A5 where C would get 0!
Finally, under regime e, the best move for A is A4:
A can convince B to make the move B1 after A makes the move A4, becuase the
score will then be (9 5 2 0), the best result for both A and B. B here agrees to give up
on the result of 10 so that A will agree to move to A4 (and A gets 9).
4) (Game-tree search - alpha-beta pruning - 15%)
a) Give an example of a 4-ply game tree (branching factor 2)
where alpha-beta pruning saving is maximal. How many nodes are pruned?
ANSWER: the best pruning is achived in:
MIN MAX MIN
A1 90 -- B1 90 -- A1 90 ----- B1 100
\ \ ----- B2 90
\ --- A2 10- ---- B1 10
\ ----- B2 40 (pruned, MAX will never let this be reached))
- B2 95+ -- A1 95+ ---- B1 100
\ ----- B2 95
--- A2 ----- B1 10 (pruned, no need to check A2 and sub-branches)
----- B2 20 (pruned)
A2 80- - B1 80- -- A1 80- ---- B1 80
\ \ ----- B2 70 (pruned)
\ --- A2 65 ----- B1 65
\ ----- B2 0 (pruned)
B2 ---- A1 ----- B1 -80 (Pruned sub-tree, as A2 top level is inferior anyway)
\ ----- B2 -90 (pruned)
--- A2 ----- B1 -100 (pruned)
----- B2 -10 (pruned)
b) Suppose that we know ahead of time that the terminal values can only
be integers between -1 and 1. Is there a case where alpha-beta can save even
more search than the best case above (show it, or prove that it cannot help).
ANSWER:
Indeed, possible. See below an example (with a limit between -100 to 100, to modify to limits above
divide all numbers by 100). Other opportunities for additional pruning also exist.
MIN MAX MIN
A1 100-- B1 100 -- A1 100----- B1 100
\ \ ----- B2 100
\ --- A2 ----- B1 10 (pruned)
\ ----- B2 40 (pruned, MAX will never let this be reached))
- B2 95+ -- A1 95+ ---- B1 100
\ ----- B2 95
--- A2 ----- B1 10 (pruned, no need to check A2 and sub-branches)
----- B2 20 (pruned)
A2 80- - B1 80- -- A1 80- ---- B1 80
\ \ ----- B2 70 (pruned)
\ --- A2 65- ---- B1 65
\ ----- B2 0 (pruned)
B2 ---- A1 ----- B1 -80 (Pruned sub-tree, as A2 top level is inferior anyway)
\ ----- B2 -90 (pruned)
--- A2 ----- B1 -100 (pruned)
----- B2 -10 (pruned)
c) Provide an example of a 2-ply + 1 chance nodes level game tree where
one can apply an adapted alpha-beta to prune some nodes. Then change the probabilities
so that no pruning is possible.
ANSWER: assume that scores are limited by 10 in absolute value (otherwise, no pruning is
possible). We will let the chance be biased. Let the deterministic case be:
CHANCE MIN
A1 7.1-- .9 9---- B1 9
\ ---- B2 10
- .1 -10---- B1 -10
A2 <=1-- .9 <=0--- B1 0
\ ---- B2 5 (pruned, as well as anything below. A will not pick A2 anyway)
--- .1 X---- B1 5
---- B2 8
So A can pick A1 to get 7.1 expected value, no need to continue checking below A2.
Changing the branch distributions to go the other way, we get:
CHANCE MIN
A1 -8.1- .1 9---- B1 9
\ ---- B2 10
- .9 -10---- B1 -10
A2 4.5-- .1 0---- B1 0
\ ---- B2 5
--- .9 5---- B1 5
---- B2 8
In this case, A will pick A2 but cannot stop the search before
checking everything below A2.
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) or (A and B and C and D and E)
b) (A or B or C or D or E) and (not A or not B or not C or not D or not E)
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)) -> not C
e) not ((A and (A -> B) and (B -> C)) -> C)
f) (A -> not A) and (not A -> A)
g) (A and (A -> B) and (B -> C)) -> C
ANSWERS:
a) Satisfiable, 3 models (one from the left part, 2 from the right part, and they do not overlap)
b) Satisfiable, 30 models (each of the clauses has 2^5-1 models, but they do not ALL overlap)
c) Not satisfiable, as at the end we have "and" with a false clause.
d) Satisfiable, 7 models (only (A, B, C) is not a model)
e) Not satisfiable: negation of a tautology (g)
f) Not satisfiable: same as (not A and A)
g) Tautology
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).
6) (FOL and situation calculus - 40%)
We need to represent and reason within the scenario defined by assignment 1.
For simplicity, we will ignore the issue of action costs, and assume only one agent.
a) Write down the axioms for the behavior of the world using FOL and
situation calculus.
Use the predicates:
Edge(e, v1, v2) ; e is an edge in the graph between v1 and v2.
Goal(v) ; Vertex v is a goal site.
Weight(e, w) ; The weight of edge e is w.
Also use the fluents (situation-dependent predicates)
Loc(v,s) ; Agent is at vertex v in situation s
Carrying(k,s) ; Agent is carrying key of type k in situation s.
Lock(v,k,s) ; Lock of type k at vertex v in situation s.
Key(v,k,s) ; Key of type k at vertex v in situation s.
Constants: as needed, for the edges and vertices, and simple actions (noop).
Functions:
traverse(e) ; Denotes a traverse move action across edge e (may be ineffective)
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, G)
Edge(E4, V1, G)
Weight(E1,1)
Weight(E2,1)
Weight(E3,1)
Weight(E4,4)
Goal(G)
; with situation S0 fluents being (note that this is a partial, "closed worlf assumption" description).
Loc(V0, S0)
Lock(V2, Fifi, S0)
Key(V1, Fifi, S0)
ANSWER:
Need to add some "closed world assumption" facts, such as: "no more locks"
forall x, y Lock(x,y,S0) => x=V2
forall x, y Lock(x,y,S0) => y=Fifi
Axioms on equality:
forall x x=x
not V1=V2 ; and similar
forall x,y,s y=x => (Carrying(x,s) => Carrying(y,s))
Also, edges are bidirectional, and one way to handle that is to add:
forall e, v1, v2 Edge(e, v1, v2) => Edge(e, v2, v1)
Also suggest to add an auxiliary predicate OK(action, from, to, situation) for legal moves:
forall s, e v1, v2 (Loc(v1, s) and Edge(e, v1, v2) and (not exists l Lock(v2, l, s) and not Carrying(l, s)))
=> OK(traverse(e),v1,v2,s)
Axiom for traversal:
forall s, e, v1, v2, l OK(traverse(e),v1,v2,s) =>
Loc(v2, Result(traverse(e), s)) and not Lock(l, v2, Result(traverse(e), s))
Axioms for picking up keys:
forall s, e, v1, v2, l OK(traverse(e),v1,v2,s) and Key(l, v2, s)
=> Carrying(l, Result(traverse(e), s))
Axioms for using keys:
forall s, e, v1, v2, l Lock(l, v2, s) and not Key(l, v2, s) and OK(traverse(e),v1,v2,s) =>
not Carrying(l, Result(traverse(e),s)
Can only be at one location at a time:
forall s, l1, l1 (Loc(l1,s) and Loc(l1,s)) => l1=l2
Frame axiom: locks do not appear magically:
forall s, v, l, a Lock(l, v, Result(a, s)) => Lock(l, v, s)
Frame axiom: locks do not disappear magically:
forall s, v, l, a Lock(l,v,s) and not Loc(v,Result(a,s)) => Lock(l, v, Result(a, s))
Frame axiom: keys do not disappear magically:
forall s, a, l, v Carrying(l, s) and Loc(v, Result(a,s)) and not Lock(l, s) => Carrying(l, Result(a,s))
Frame axiom: keys do not appear magically:
forall s, a, l, v Carrying(l, Result(a,s)) => (Carrying(l, s) or (Loc(v,Result(a,s)) and Key(l,v,s)))
b) Now, we need to find a sequence of actions that will result in reaching the goal optimally
from S0 (which you found in question 1 above), and prove a theorem that it will
reach the goal (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).
ANSWER:
Edge bidirectionality becomes:
1. not Edge(e, v1, v2) or Edge(e, v2, v1)
Closed world assumption on locks:
2. x=V2 or not Lock(x, y, S0)
2a. y=Fifi or not Lock(x, y, S0)
Equality axiom:
2=. not y=x or not Carrying(x,s) or Carrying(y,s)
Axiom for OK predicate becomes:
3a. not Loc(v1, s) or not Edge(e, v1, v2) or Lock(v2, L(v1,v2,e,s),s) or OK(traverse(e),v1,v2,s)
3b. not Loc(v1, s) or not Edge(e, v1, v2) or not Carrying(L(v1,v2,e,s),s) or OK(traverse(e),v1,v2,s)
Note that L(v1,v2,e,s) is a Skolem function due to the existential quantifier.
Traversal axiom becomes:
4a. not OK(traverse(e),v1,v2,s) or Loc(v2,Result(traverse(e),s))
4b. not OK(traverse(e),v1,v2,s) or not Lock(l, v2, Result(traverse(e), s))
Axiom for picking up keys:
5. not OK(traverse(e),v1,v2,s) or not Key(l, v2, s) or Carrying(l, Result(traverse(e), s))
Axiom for using key will not be needed in proof.
Frame axiom for non-appearance of locks:
6. not Lock(v, l, Result(a, s)) or Lock(v, l, s)
Frame axiom for keys not disappearing:
7. not Carrying(l, s) or not Loc(v, Result(a,s)) or Lock(v, l, s) or Carrying(l, Result(a,s))
The other frame axioms not needed in proof.
B) Formally list what we need to prove (a theorem), and state its negation.
ANSWER: The optimal path was "Go to V1, go to V0, Go to V2, Go to G" which is:
"traverse E1 (twice), traverse E2, Traverse E3" so need to prove:
Exists x Goal(x) and Loc(x,Result(traverse(E3),Result(traverse(E2),Result(traverse(E1),Result(traverse(E1),S0)))))
Its negation, after converting to CNF is:
Q':not Goal(x) or not Loc(x,Result(traverse(E3),Result(traverse(E2),Result(traverse(E1),Result(traverse(E1),S0)))))
C) Use resolution to reach a contradiction, thus proving the theorem.
At each step of the proof, specify the resolvents and the unifier.
ANSWER:
There are many ways to do it. We will do one of the shortest ones.
Resolve "not V1=V2" with 2, unifier {x|V1} to get:
10. not Lock(V1, y, S0)
Resolve 10 with 3a, unifier {v2|V1, s|S0, y|L(v1,v2,e,s)} to get:
11. not Loc(v1, S0) or not Edge(e, v1, V1) or OK(traverse(e),v1,V1,S0)
Resolve 11 with initial situation fact "Loc(V0, S0)" unifier {v1|V0} to get:
12. not Edge(e, V0, V1) or OK(traverse(e),V0,V1,S0)
Resolve 12 with "Edge(E1, V0, V1)", unifier {e|E1} to get:
13. OK(traverse(E1),V0,V1,S0)
Meaning that traversing E1 in S0 will "succeed".
Now we prove that the agent gets to V1 and picks up the key.
Resolve 13 with 4a, unifier {e|E1,v1|V0,v2|V1,s|S0} to get:
14. Loc(V1,Result(traverse(E1),S0))
Likewise, resolve 13 with 5, same unifier, to get:
15. not Key(V1, l, S0) or Carrying(l, Result(traverse(E1), S0))
and resolve 15 with initial fact: "Key(V1, Fifi, S0)" unifier {l|Fifi} to get:
16. Carrying(Fifi, Result(traverse(E1), S0))
We can continue this way to prove location of the agent in subsequent situations.
Resolve 1 with "Edge(E1, V0, V1)" unifier {e|E1,v1|V0,v2|V1} to get (the reverse edge):
17. Edge(E1, V1, V0)
Now need to show no locks at V0 after the first traversal, so we can get back (need frame axiom!)
Resolve "not V0=V2" with 2, unifier {x|V0} to get:
18. not Lock(V0, y, S0)
Now resolve 18 with frame axiom 6, unifier {v|V0, s|S0, y|l} to get:
19. not Lock(V0, l, Result(a, S0))
Now to show that it is OK to traveres E1 backwards.
Resolve 17 with 3a, unifier {e|E1,v1|V1,v2|V0} to get:
20. not Loc(V1, s) or Lock(V0, L(V1,V0,E1,s),s) or OK(traverse(E1),V1,V0,s)
Now resolve 19 with 20, unifier {l| L(V1,V0,E1,s), s|Result(a, S0)} to get:
21. not Loc(V1, Result(a, S0)) or OK(traverse(E1),V1,V0,Result(a, S0))
Resolve 14 with 21, unifier {a|traverse(E1)} to get:
22. OK(traverse(E1),V1,V0,Result(traverse(E1), S0))
So now the action of traversing E1 back is proved OK, show properties of resulting situation
(at V0, and still carrying key). Resolve 22 with 4a, unifier {e|E1,v1|V1,v0|V2,s|Result(traverse(E1), S0)} to get:
23. Loc(V0, Result(traverse(E1), Result(traverse(E1),S0)))
We now introduce convenience shorthand, so as to reduce clutter,
use the string "RR" to mean "Result(traverse(E1), Result(traverse(E1),S0))"
and "R" to mean "Result(traverse(E1),S0)",
just to make everything shorter, as we need to repeat these strings many times in the proof.
To likewise show we still have the key, resolve (frame axiom!) 7 with 19,
unifier {v|V0,s|Result(a,S0)} to get (note standardizing apart of the "a" variable):
24: not Carrying(l, Result(a,S0)) or not Loc(V0, Result(a1,Result(a,S0))) or Carrying(l, Result(a1,Result(a,S0))))
Resolve 16 with 24, unifier {l|Fifi,a|traverse(E1)} to get:
25: not Loc(V0, Result(a1,Result(traverse(E1),S0))) or Carrying(Fifi, Result(a1,Result(traverse(E1),S0)))
Resolve 25 with 23, unifier {a|traverse(E1)} to get:
26. Carrying(Fifi, Result(traverse(E1),Result(traverse(E1),S0)))
or in shorthand: Carrying(Fifi,RR)
Now we need to show that we can traverse E2 in situation RR. We know the agent location,
and that it is carrying Fifi. Then we can prove that the traversal is OK, and that the agent gets to V2.
Resolve frame axiom 6 with 2a, unifier {x|v, y|l,s|S0} to get:
27: l=Fifi or not Lock(v, l, Result(a, S0))
Resolve 27 again with 2a, unifer {x|v, y|l,s|Result(a, S0)} to get:
28: l=Fifi or not Lock(v, l, Result(a1,Result(a, S0)))
Note that again we standardize apart the "a" variables, but also drop one "l=Fifi" as it is a repetition.
Resolve 28 again with 2a, unifer {x|v, y|l,s|Result(a1,Result(a, S0))} to get:
29: l=Fifi or not Lock(v, l, Result(a2,Result(a1,Result(a, S0))))
That is, after 3 actions the only lock anywhere must (still) be Fifi.
Now resolve 3b with 23, unifier {v1|V0, s|RR} to get
30. not Edge(e, V0, v2) or not Carrying(L(V0,v2,e,RR),RR) or OK(traverse(e),V0,v2,RR)
Resolve "Edge(E2,V0,V2)" with 30, unifier {e|E2,v2|V2} to get:
31. not Carrying(L(V0,V2,E2,RR),RR) or OK(traverse(E2),V0,V2,RR)
Resolve 3a with "Edge(E2,V0,V2)", unifier {e|E2,v1|V0,v2|V2} to get:
32. not Loc(V0, s) or Lock(V2, L(V0,V2,E2,s),s) or OK(traverse(E2),V0,V2,s)
Resolve 32 with 23, unifier {s|RR} to get:
33. Lock(V2, L(V0,V2,E2,RR),RR) or OK(traverse(E2),V0,V2,RR)
Resolve 33 with 29, unifier {v|V2, l|L(V0,V2,E2,RR),s|RR} to get:
34. L(V0,V1,E2,RR)=Fifi or OK(traverse(E2),V0,V2,RR)
Resolve equality axiom 2= with 34, unifier {x=L(V0,V2,E2,RR), y=Fifi, s=RR} to get:
35. not Carrying(Fifi,RR) or Carrying(L(V0,V1,E2,RR),RR) or OK(traverse(E2),V0,V2,RR)
Resolve 26 with 35, empty unifier, to get:
36. Carrying(L(V0,V2,E2,RR),RR) or OK(traverse(E2),V0,V2,RR)
Resolve 36 with 31, empty unifier, to get:
37. OK(traverse(E2),V0,V2,RR)
Now that the traversal is proved OK, we can prove properties after traversal.
Resolve 37 with 4a, unifier {e|E2, v1|V0, v2|V2, s|RR} to get:
38. Loc(V2,Result(traverse(E2),RR))
Denote "Result(traverse(E2), Result(traverse(E1), Result(traverse(E1),S0)))" by RRR (another shorthand).
Having proved that the agent got to V2, we need to prove that in situation RRR
there is no lock at G, and then we can prove that traversing E3 will work,
and then we can finally prove that the agent gets to G.
Resolve CWA 2 with "not G=V2", unifier {x|G} to get:
40. not Lock(G,y, S0)
Resolve 40 with (frame axiom) 6, unifier {v|G, s|S0, l|y} to get:
41. not Lock(G, y, Result(a,S0))
Resolve 41 with 6, unifier {v|G,s|Result(a,S0), l|y} to get (again, standardize apart the "a"):
42. not Lock(G, y, Result(a1, Result(a,S0)))
Resolve 42 with 6, unifier {v|G,s|Result(a1, Result(a,S0)), l|y} to get (again, standardize apart the "a"):
43. not Lock(G, y, Result(a2, Result(a1, Result(a,S0))))
OK, proved no lock at G after 3 actions, no to show that traversal is OK:
Resolve "Edge(E3, V2, G)" with 3a, unifier {v1|V2, v2|G, e|E3} to get:
44. not Loc(V2, s) or Lock(G, L(V2,G,E3,s),s) or OK(traverse(E3),V2,G,s)
Resolve 44 with 38, unifier {s|RRR} to get:
45. Lock(G, L(V2,G,E3,RRR),RRR) or OK(traverse(E3),V2,G,RRR)
Resolve 45 with 43, unifier {y|L(V2,G,E3,RRR), Result(a2, Result(a1, Result(a,S0)))|RRR}
where the latter sunstitution means {a2|traverse(E2), a1|traverse(E1), a|traverse(E1)} to get:
46. OK(traverse(E3),V2,G,RRR)
Now to prove the final location, resolve 46 with 4a, unifier {e|E3, v1|V2, v2|G, s|RRR} to get:
47. Loc(G, Result(traverse(E3), RRR))
Finally, resolve 48 with Q', unifier {x|G} to get:
48. not Goal(G)
and resolve 48 with the scenario axiom "Goal(G)" to get the empty clause (contradiction), and we are done.
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?
ANSWER:
See above that we had to use frame axioms in several steps: showing that we are still carrying
the key after returning to V0, and axioms stating that locks do not appear.
There would be no way to prove the result without these axioms.
d) Would we be able to do the proof using only forward chaining?
ANSWER:
We attempted to use only the "forward" direction. Therefore, if we used only Horn clauses
with unit resolution the answer is yes. So examine the proof...
It seems that we had to use 3a, which has 2 positive literals and this is NOT a Horn clause.
Also, 3a is essential and forward chaining cannot use it, and so the answer is no.
Same problem w.r.t. frame axiom 7, also used in the proof and unavoidable.
Justify all answers shortly!
Deadline: (16:00), Tuesday, December 13, 2016 ( strict deadline).
Submissions are to be solo.