1) (agents and environment simulators)
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 Tic-Tac-Toe.
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 coordination agent (sets meetings between humans with conflicting goals).
e) An agent that can play peg-and-hole solitaire.
f) An agent that plays Go optimally.
ANSWERS:
a) Poker: environment is stochastic (dealing cards), inaccessible, discrete (but money is "almost" continuous),
static, non-episodic (can learn between deals), and multi-agent. Needs a utility based agent (with
learning). The "stochastic" part can be cast into "inacessibility" (cards have been dealt, but unknown)
making it "deterministic", but this does not help.
b) Tic-tac-toe: environment is deterministic, accessible, discrete, static,
episodic, and multi-agent. Goal-based agent can be used, but this problem is small enough that
can use a reflex agent, even with table lookup.
c) DRC: environment is stochastic, inaccessible, continuous, dynamic, non-episodic, and multi agent (operator and
robot). Needs a utility based agent (with learning).
d) Internet coordination: environment is stochastic, inaccessible, discrete (almost), dynamic, non-episodic, and multi agent.
Needs a utility-based agent due to possible conflicts between agents.
e) Peg and hole solitaire: environment is detreministic, accessible, static, episodic, and single agent. A goal-driven agent suffices.
f) Go: environment is detreministic, accessible, static, episodic, and multi agent. (Possibly non-episodic for
repeated games if we allow learning of opponent strategy). Needs a goal-based or utility-based agent,
although it is only recently that search based agents do significantly better than rule-based.
2) (Search):
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 V2 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 is always carrying exactly the minimal amount of food needed to cross
an edge before traversing it (i.e. shortest path in the graph of edges with the weights squared).
a) Greedy search (f(n) = h(n)), breaking ties in favor of states where the
higher node number.
ANSWER:
We will represent the state by the tuple (loc, food carried, food at V1) as these are the only
relevant variable. We will assume that the successor function does not generate
states where the agent is dead.
S0: (V0, 1, 3) g=0, h=4, f=4
Not a goal state, so we expand by acrions noop and traverse(E1) (traverse(E2) kills the agent so
is not generated), and we have:
S1: (V0, 0, 3) g=1, h=4, f=5 ; with noop
S2: (V1, 3, 0) g=1, h=5, f=9 ; travese E1
So now we expand the lowest h value S1 but it not a goal and has no successors (agent dies with every action).
So we expand S2, where noop and traversal are legal, to get:
S3: (V1, 2, 0) g=2, h=5, f=7 ; with noop
S4: (V0, 2, 0) g=5, h=4, f=9 ; traverse E1
So now we expand S3, which is not a goal, to add:
S5: (V0, 1, 0) g=6, h=4, f=10 ; with noop
S6: (V1, 1, 0) g=7, h=5, f=12 ; traverse E1
S7: (V2, 0, 0) g=9, h=0, f=9 ; traverse E2
The lowest h value is 0 for S7, which is picked. Since it is a goal, we are done.
Thos happens to result in the optimal solution: traverse E1 (to get food), traverse E1 (back), traverse E3.
b) A* search, (f(n) = g(n)+h(n)), breaking ties as above.
ANSWER:
S0: (V0, 1, 3) g=0, h=4, f=4
Not a goal state, so we expand by acrions noop and traverse(E1) (traverse(E2) kills the agent so
is not generated), and we have:
S1: (V0, 0, 3) g=1, h=4, f=5 ; with noop
S2: (V1, 3, 0) g=1, h=5, f=9 ; travese E1
So now we expand the lowest f value S1 but it not a goal and has no successors (agent dies with every action).
So we expand S2, where noop and traversal are legal, to get:
S3: (V1, 2, 0) g=2, h=5, f=7 ; with noop
S4: (V0, 2, 0) g=5, h=4, f=9 ; traverse E1
So now we expand S3, which is not a goal, to add:
S5: (V1, 1, 0) g=3, h=5, f=8 ; with noop
S6: (V0, 1, 0) g=4, h=4, f=8 ; traverse E1
So now we expand S5 (tie breaking rule), which is not a goal, to get:
S7: (V1, 0, 0) g=4, h=5, f=9 ; with noop
S8: (V0, 0, 0) g=4, h=4, f=8 ; traverse E1
We now have S6, S8 with f=8, and location V0, cannot discriminate, say we pick
S8. It is not a goal and has no successors, so we pick S6. It is not a goal, so is expanded
to get:
S9: (V0, 0, 0) g=5, h=4, f=9 ; with noop
S10: (V1, 0, 0) g=5, h=5, f=10 ; traverse E1
We are done with f=8, and move to f=9, with tie breaking we pick S7.
It is not a goal, and no successors, so now we pick either S4 or S7 or S9.
Suppose we pick S9, which is not a goal, so we add:
S11: (V0, 1, 0) g=6, h=4, f=10 ; with noop (can be discarded with duplicate checking)
S12: (V1, 1, 0) g=7, h=5, f=12 ; traverse E1
S13: (V2, 0, 0) g=9, h=0, f=9 ; traverse E2
Now we have several f=9 to pick from, but tie breaking prefers S13
which is a goal so we are done, and have found the optimal solution.
c) Simplified RTA* with a limit of 2 expansions per real action, breaking ties as above.
ANSWER:
With RTA* we begin with:
S0: (V0, 1, 3) g=0, h=4, f=4
Not a goal state, so we expand by acrions noop and traverse(E1) (traverse(E2) kills the agent so
is not generated), and we have:
S1: (V0, 0, 3) g=1, h=4, f=5 ; with noop
S2: (V1, 3, 0) g=1, h=5, f=9 ; travese E1
So now we expand the lowest f value S1 but it not a goal and has no successors (agent dies with every action).
Now must move, and S1 is known to be a dead end, so go towards S2 i.e. traverse E1.
After the move, we re-start:
So we expand S2 (the "new S0"), where noop and traversal are legal, to get:
S3: (V1, 2, 0) g=2, h=5, f=7 ; with noop
S4: (V0, 2, 0) g=5, h=4, f=9 ; traverse E1
So now we expand S3, which is not a goal, to add:
S5: (V1, 1, 0) g=3, h=5, f=8 ; with noop
S6: (V0, 1, 0) g=4, h=4, f=8 ; traverse E1
Now must return a move, towards either S5 or S6, i.e. noop.
We are now at S3, so start again: expand S3, which is not a goal, to add:
S5: (V1, 1, 0) g=3, h=5, f=8 ; with noop
S6: (V0, 1, 0) g=4, h=4, f=8 ; traverse E1
So now we expand S5 (tie breaking rule), which is not a goal, to get:
S7: (V1, 0, 0) g=4, h=5, f=9 ; with noop
S8: (V0, 0, 0) g=4, h=4, f=8 ; traverse E1
Now we move towards either S6 or S8. This continues for several more expansions,
and then gets stuck as food runs out!
d) Repeat a-c but using h'(n) = 2*h(n) as the heuristic. Is h'(n) admissible?
ANSWER: for greedy heuristic search, exactly the same using h(n) because the
order of expansions is based only on the heuristic (but double all the h values).
For A*, we have:
S0: (V0, 1, 3) g=0, h'=8, f=8
Not a goal state, so we expand by acrions noop and traverse(E1) (traverse(E2) kills the agent so
is not generated), and we have:
S1: (V0, 0, 3) g=1, h'=8, f=9 ; with noop
S2: (V1, 3, 0) g=1, h'=10, f=11 ; travese E1
So now we expand the lowest f value S1 but it not a goal and has no successors (agent dies with every action).
So now we expand S2, where noop and traversal are legal, to get:
S3: (V1, 2, 0) g=2, h'=10, f=12 ; with noop
S4: (V0, 2, 0) g=5, h'=8, f=13 ; traverse E1
So now we expand S3, which is not a goal, to add:
S5: (V1, 1, 0) g=3, h'=10, f=13 ; with noop
S6: (V0, 1, 0) g=4, h'=8, f=12 ; traverse E1
So now we expand S6, which is not a goal, to get:
S7: (V0, 0, 0) g=5, h'=8, f=13 ; with noop
S8: (V1, 0, 0) g=5, h'=10, f=15 ; traverse E1
So now we pick S5 (due to tie breking), and expand to get:
S9: (V1, 0, 0) g=4, h'=10, f=14 ; with noop
S10: (V0, 0, 0) g=4, h'=8, f=12 ; traverse E1
We pick S10 it is no goal and no successors, so now
We are done with f=12, and move to f=13, with tie breaking we pick either S4 or S7.
Picking S7, not a goal and no successor, so now S4.
It is not a goal, so expand to get:
S11: (V0, 1, 0) g=6, h'=8, f=16 ; with noop (can be discarded with duplicate checking)
S12: (V1, 1, 0) g=7, h'=10, f=17 ; traverse E1
S13: (V2, 0, 0) g=9, h'=0, f=9 ; traverse E2
Now we have S13 with f=9, and it is a goal so we are done and
have found the optimal solution.
This is despite the fact that h' is not admissible, e.g. it returns h=8 in S4 despite the fact that
the cost to the goal there is only 4.
With RTA* we begin with:
S0: (V0, 1, 3) g=0, h'=8, f=8
Not a goal state, so we expand by acrions noop and traverse(E1) (traverse(E2) kills the agent so
is not generated), and we have:
S1: (V0, 0, 3) g=1, h'=8, f=9 ; with noop
S2: (V1, 3, 0) g=1, h'=10, f=11 ; travese E1
So now we expand the lowest f value S1 but it not a goal and has no successors (agent dies with every action).
So move to S2, which becomes the "new S0".
Now we expand S2, where noop and traversal are legal, to get:
S3: (V1, 2, 0) g=2, h'=10, f=12 ; with noop
S4: (V0, 2, 0) g=5, h'=8, f=13 ; traverse E1
So now we expand S3, which is not a goal, to add:
S5: (V1, 1, 0) g=3, h'=10, f=13 ; with noop
S6: (V0, 1, 0) g=4, h'=8, f=12 ; traverse E1
The best here is again S6, and the first move is noop which is executed.
So again we eventually get stuck.
3) (Game trees):
Consider a 3-person game (A, B, C) with complete information and deterministic environment.
Suppose A has 5 possible moved. 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) B and C may agree on a deal if it is beneficial to both of them
c) B and C may agree on a deal if it is nebeficial to both, but C is
allowed to violate it (but B does not know that).
d) A and B may reach a deal, if it is beneficial to both of them
e) As in a, but in case of tie-breaking do a move that is worse for A.
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) scores, respectively).
A1 ----- B1 ---- C1 ----- (7 2 5)
C2 ----- (0 0 2)
B2 ---- C1 ----- (4 3 9)
C2 ----- (4 0 10)
B3 ---- C1 ----- (4 2 5)
A2 ----- B1 ---- C1 ----- (2 2 5)
C2 ----- (0 0 2)
B2 ---- C1 ----- (4 3 9)
C2 ----- (8 0 10)
A3 ----- B1 ---- C1 ----- (6 0 0)
B3 ---- C1 ----- (4 0 0)
A4 ----- B1 ---- C1 ----- (9 5 0)
B2 ---- C1 ----- (0 10 0)
A5 ----- B1 ---- C1 ----- (5 0 0)
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, to get (7 2 5), i.e. a score of 7 for A.
This is the best A can get anywhere under this regime. (Assuming ties are broken in favor of A).
Under regime b, the best move for A is A3: 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), so A will only get 4, and as a result
the best move for A is A3 which earns 6 for A. (Assuming B breaks ties IN FAVOR of A).
(Doing A2 will cause the deal between B and C to be (4 3 9) which is also not good for A.
Under regime c, the best move for A is A2: B and C make the same deal for either A1 or A2.
But since C will renege on the deal,
(in order to get 10 instead of 9 after the moves A1B2 or A2B2), then it is better for A to take the
move A2, because after B does B2 and C reneges and does C2, the score will be (8 0 10), so A will get 8,
the best available score here.
Under regime d, 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), 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).
Finally, consider issue e where ties are broken against A. Here it is no good to make moves A1 or A3
because then B will take move B3 and A will get only 4. So the best move for A is A5 which gains 5 for A.
4) (Game-tree search - alpha-beta pruning)
a) Give an example of a 3-ply game tree (branching factor 2)
where alpha-beta pruning saving is maximal. How many nodes are pruned?
b) Suppose that we know ahead of time that the terminal values can only
be integers between -10 and 10. 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).
c) Provide an example of a 2-ply + 2 chance nodes level game tree where
one can apply an adapted alpha-beta to prune some nodes,
and a similar example where changing the distribution on the chance node
edges results in no savings for pruning.
ANSWER:
a) In case below, 2 nodes pruned at bottom, but also prunes a branch at level 2.
MIN MAX
A1 10 -- B1 10 -- 10
\ \
\ --- 1
\
- B2 10+ -- 10
\
--- (pruned, because MIN can force 109, which is not greater than 10)
A2 8- -- B1 8- -- 8
\ \
\ --- (pruned, because MIN can force 8, which is less than 10)
\
B2 (pruned, because MAX can get 10, which is more than 8)
b) In the same examle as above, can now prune the entire subtree below A2, as A already
has a move which guarantees 10, the maximum score.
c) assume that scores are limited by 11 in absolute value. (If there are no bounds, cannot prune.)
We will let the chance be biased.
CHANCE MIN CHANCE
A1 7.1-- .9 9---- B1 9 -- .5 11
\ \ -- .5 9
\ --- B2 10 -- .5 0
\ -- .5 10
- .1 -10---- B1 -10 -- .5 -10
-- .5 -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 0
So A can pick A1 to get 7.1 expected value, no need to continue checking below A2.
Changing the branch distributions at the top-level chance nodes to go the other way, we get:
CHANCE MIN CHANCE
A1 -8.1- .1 9---- B1 9 -- .5 11
\ \ -- .5 9
\ --- B2 10 -- .5 0
\ -- .5 10
- .9 -10---- B1 -10 -- .5 -10
-- .5 -10
A2 0---- .1 0---- B1 0 -- .5 5
\ \ -- .5 -5
\ -- B2 5 -- .5 0
\ -- .5 10
-- .9 0---- B1 5 -- .5 0
\ -- .5 10
--- B2 0 -- .5 -10
-- .5 10
In this case, A will pick A2 but cannot stop the search before
5) (Propositional logic)
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). Bonus question: in case b, also trace the run of the DPLL algorithm for satisfiability with this
formula as input (i.e. explain any recursive calls and cases encountered).
a) (A and (A -> B) and (B -> C)) -> C
b) (A or not B or D) and (not A or B) and (not A or not B or D) and (A or not B)
c) (A or B or C or D or E or F)
d) (A and not A) and (Not B)
e) (A and (A -> B) and (B -> C)) -> not C
f) not ((A and (A -> B) and (B -> C)) -> C)
g) A -> not A
ANSWERS:
a) Valid, so 8 models, since there are 3 variables.
b) Satisfiable, 2 models: (A=B=TRUE, D=TRUE) and (A=B=FALSE, D=TRUE). D must be true because otherwise
every assignment to A and B will falsify some clause.
c) Satisfiable 63 models (6 variables, and only one assignment is not satisfying, so 2^6-1)
d) Unatisfiable. The first part is false regardless of the value of A, and the "and" then
causes the sentence to be false.
e) Satisfiable. Holds if not C (4 models), and also if the antecedent is false, which it is unless A,B,C=true,
resulting in 7 models. But all the models of not C overlap them. So total 7 models.
f) Unsatisfiable, since it is a negation of a valid formula.
g) Satisifable, one model: A=false
6) (FOL and situation calculus)
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 Yazidi refugee 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.
Also use the fluents (situation-dependent predicates)
Loc(v,s) ; Agent is at vertex v in situation s
Carrying(f,s) ; Agent is carrying f units of food in situation s.
Food(v,f, s) ; There are f units of food at vertex v in situation s.
Constants: as needed, for the edges and vertices, and simple actions (noop).
Functions:
weight(e) ; Function denoting the weight of edge e
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.
In this assignment you will need arithmetic functions and predicates, be sure to define them formally!
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, V1, V2)
Edge(E3, V0, V2)
Goal(V2)
Weight(E1)=1
Weight(E2)=4
Weight(E3)=2
; with situation S0 fluents being:
Loc(V0, S0)
Food(V1,3,S0)
Food(V0,0,S0)
Food(V2,0,S0)
Carrying(1,S0)
ANSWER: We will add predicate Alive(s) denoting that the agent is alive. We will also need the arithmetic predicate geq
(greater or equal) and the arithmetic function +.
Axioms for Alive are:
1: forall a, s, not Alive(s) => not Alive(Result(a, s))
2: forall a, s, Alive(s) and FoodOK(a, s) => Alive(Result(a, s))
3: forall a, s, not FoodOK(a, s) => not Alive(Result(a, s))
4: Alive(S0)
Where FoodOk is an auxialiary predicate to be defined below.
Actions are noop (a constant) and traverse(e). Note that syntactically traverse is a function symbol.
The rules for FoodOK:
5: forall s, f, Alive(s) and Carrying(f, s) and geq(f,1) => FoodOK(noop, s)
6: forall s, e, f, Alive(s) and Carrying(f, s) and geq(f,weight(e)) => FoodOK(travese(e), s)
Now the rules for food consumption for noop:
7: forall s, f, Carrying(f+1, s) and FoodOK(noop, s) => Carrying(f, Result(noop, s))
The latter assues NO FOOD PICKUP and will need to be fixed later!
The rules for traversal:
8: forall s, e, v1, v2 Alive(s) and FoodOK(traverse(e),s) and Edge(e, v1, v2) and Loc (v1, s) => Loc(v2, Result(traverse(e), s))
9: forall s, e, v1, v2 Alive(s) and FoodOK(traverse(e),s) and Edge(e, v1, v2) and Loc (v2, s) => Loc(v1, Result(traverse(e), s))
And for food pickup:
10: forall s, e, v1, v2 Alive(s) and FoodOK(traverse(e),s) and weight(e)= f2 and carrying(f+f2, s) and Edge(e, v1, v2) and Loc (v1, s) and Food(v2, f1, s)
=> Food(v2, 0, Result(traverse(e), s)) and Carrying(f+f1, Result(travese(e), s))
11: forall s, e, v1, v2 Alive(s) and FoodOK(traverse(e),s) and weight(e)= f2 and carrying(f+f2, s) and Edge(e, v1, v2) and Loc (v2, s) and Food(v1, f1, s)
=> Food(v1, 0, Result(traverse(e), s)) and Carrying(f+f1, Result(travese(e), s))
Note how this is inelegant because all axioms are repeated for each possible (source, destination) order of the vertices!
We must also axiomitize illegal actions, but will ignore it as this will not be needed for the proofs. Must
also axiomatize "geq" and the "+" function. We can also go for the partial, finite axiomatization by adding the facts,
with SOME general axioms such as transitivity of geq (we will not number them):
forall x, y, z geq(x,y) and geq(y,z) => geq(x,z)
forall x, y x+y => y+x
forall x, y x=y => y=x
forall x, y, z x=y and y=z => x=z
etc.
Now some basic arithmetic facts:
0=0
1=1
2=2
3=3
not 0=1
not 1=2
not 2=3
0+1=1
1+2=3
geq(1,0)
geq(2,1)
geq(3,2)
etc.
(For people using the integer successor function, you can write:
forall x geq(S(x),x)
this takes care of the geq predicate, together with the above transitivity axiom for geq)
Also need all axioms for equality such as:
forall x,y,z geq(x, y) and z=y => geq(x,z)
b) Now, we need to find a sequence of actions that will result in reaching the goal from S0,
and prove a theorem that it will do so. Do the following steps:
A) Convert the knowledge base to 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
ANSWER:
A) We will just do the necessary ones. We will avoid "standardizing apart" for now unless we must.
1: Alive(s) or Alive(Result(a, s))
2: not Alive(s) or not FoodOK(a, s) or Alive(Result(a, s))
3: FoodOK(a, s) or not Alive(Result(a, s))
4: Alive(S0)
5: not Alive(s) or not Carrying(f, s) or not geq(f,1) or FoodOK(noop, s)
6: not Alive(s) or not Carrying(f, s) or not geq(f,weight(e)) or FoodOK(travese(e), s)
8: not Alive(s) or not FoodOK(traverse(e),s) or not Edge(e, v1, v2) or not Loc (v1, s) or Loc(v2, Result(traverse(e), s))
9: not Alive(s) or not FoodOK(traverse(e),s) or not Edge(e, v1, v2) or not Loc (v2, s) or Loc(v1, Result(traverse(e), s))
Now 10 and 11 have "and" on the RHS so need to distribute, and each generates 2 clauses:
10a: not Alive(s) or not FoodOK(traverse(e),s) or not weight(e)= f2 or not carrying(f+f2, s) or not Edge(e, v1, v2) or not Loc (v1, s) or not Food(v2, f1, s)
or Food(v2, 0, Result(traverse(e), s))
10b: not Alive(s) or not FoodOK(traverse(e),s) or not weight(e)= f2 or not carrying(f+f2, s) or not Edge(e, v1, v2) or not Loc (v1, s) or not Food(v2, f1, s)
or Carrying(f+f1, Result(travese(e), s))
11a: not Alive(s) or not FoodOK(traverse(e),s) or not weight(e)= f2 or not carrying(f+f2, s) or not Edge(e, v1, v2) or not Loc (v2, s) or not Food(v1, f1, s)
or Food(v1, 0, Result(traverse(e), s))
11b: not Alive(s) or not FoodOK(traverse(e),s) or not weight(e)= f2 or not carrying(f+f2, s) or not Edge(e, v1, v2) or not Loc (v1, s) or not Food(v2, f1, s)
or Carrying(f+f1, Result(travese(e), s))
B) The solution here is traverse E1 to get food, travrese E1 back to V0, and then traverse E3 to V2.
That is, we need to prove that the agent is at a goal vertex and alive as a result of
executing this action sequence.
G: exists v Goal(v) and Loc(v, Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
and Alive(Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
Its negation is:
not exists v Goal(v) and Loc(v, Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
and Alive(Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
and converting it to normal form we get:
G': not Goal(v) or not Loc(v, Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
or not Alive(Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
C) OK, now to start the proof. We will assume that the arithmetic facts are all in basic form, so that we
do not have to prove things like geq(3,1) which actually follows from the axioms given above. Also, while
it is standard practice to start with G' in order to focus the search, there will be thing we can prove
initially that will make the proof shorter. So:
Resolve 8 with Edge(E1,V0,V1), unifier v1/V0, v2/V1, e/E1 to get:
100: not Alive(s) or not FoodOK(traverse(E1),s) or not Loc (V0, s) or Loc(V1, Result(traverse(E1), s))
Resolve 4 with 100, unifier s/S0 to get:
101: not FoodOK(traverse(E1),S1) or not Loc (V0, S1) or Loc(V1, Result(traverse(E1), S0))
Resolve "Loc(V0, S0)" with 101, null unifier, to get:
102: not FoodOK(traverse(E1),S0) or Loc(V1, Result(traverse(E1), S0))
Resolve 4 with 2, unifier s/S0 to get:
103: not FoodOK(a, S0) or Alive(Result(a, S0))
Resolve 4 with 6, unifier s/S0 to get:
104: not Carrying(f, S0) or not geq(f,weight(e)) or FoodOK(travese(e), S0)
Resolve 104 with "Carrying(1,S0)", unifier f/1, to get
105: not geq(1,weight(e)) or FoodOK(travese(e), S0)
Resolve 102 with 105, unifier e/E1 to get:
106: not geq(1, weight(E1)) or Loc(V1, Result(traverse(E1), S0))
Resolving the axiom for equality, and "geq(1,1)" we get:
107: not z=1 or geq(1,z)
Resolving 107 and "weight(E1)=1", unifier z/weight(E1) we get:
108: geq(1,weight(E1))
Resolving 108 with 106, empty unifier, we get:
109: Loc(V1, Result(traverse(E1), S0))
Resolving 108 with 105, unifier e|E1, we also get:
110: FoodOK(travese(E1), S0)
Resolving 110 with 103, unifier a/travese(E1) we get:
111: Alive(Result(travese(E1), S0))
Now we need to use 10a and 10b to prove what is the amount of food at V1 and also what amout of
food is being carried after the traversal. The former is not needed later on, so we will do the latter.
Resolve 10b with "Edge(E1, V0, V1)", unifier e|E1, v1|V0, v2|V1 to get:
112: not Alive(S0) or not FoodOK(traverse(E1),S0) or not weight(E1)= f2 or not carrying(f+f2, S0) or not Loc (V0, S0) or not Food(V1, f1, S0)
or Carrying(f+f1, Result(travese(E1), S0))
Now resolve 112 with "Alive(S0)", then with "Loc(V0,S0)", then with 110, (these are THREE SEPARATE resolution
operations, not shown for conciseness, as they are trivial) to get:
115: not weight(E1)= f2 or not carrying(f+f2, S0) or not Food(V1, f1, S0) or Carrying(f+f1, Result(travese(E1), S0))
Resolve 115 with "weight(E1)=1", unifier f2/1, to get
116: not carrying(f+1, S0) or not Food(V1, f1, S0) or Carrying(f+f1, Result(travese(E1), S0))
Resolve 116 with "Food(V1, 3, S0)", unifier f1/3, to get:
117: not carrying(f+1, S0) or Carrying(f+3, Result(travese(E1), S0))
Resolve an equality axiom: "not carrying(x,s) or not y=x or carrying(y,s)"
with "0+1=1", unifier x/1, y/0+1 to get (note the amount of annoying nitpicking needed to handle equality!)
118: not carrying(1,s) or carrying(0+1,s)
Resolve 118 with Carrying(1, S0) unifier s/S0 to get:
119: carrying(0+1,S0)
Now resolve 119 with 117, unifier f/0 to get:
120: Carrying(0+3, Result(travese(E1), S0))
Now 2 steps needed using 120 and an equality axiom (similar to above) to get:
121: Carrying(3, Result(travese(E1), S0))
Finally we have proved all (?? almost, see answer to c) statements needed for the situation Result(travese(E1), S0) and can proceed to prove
in almost exactly the same way (not repeating the steps here), that:
140: Alive(Result(travese(E1), Result(travese(E1), S0)))
160: Carrying(2,Result(travese(E1), Result(travese(E1), S0)))
180: Loc(V0,Result(travese(E1), Result(travese(E1), S0)))
And likewise now can prove, using similar steps:
200: Loc(V2, Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
220: Alive(V2, Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
Finally Resolve G' with "Goal(V2)" (unifier v/V2), then with 200, then with 220, to get the empty clause
(a contradiction), thus completing the proof.
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: We did have frame axioms for "Alive", but forgot the ones on food at vertices not
related to traverse actions! (Even though the amount of food there is ZERO, and does not
help the agent, STILL we would not be able to prove ANY "Carrying" statement for this
situation!!!) So we needed to add them above. Otherwise, will be unable to prove:
Carrying(2,Result(travese(E1), Result(travese(E1), S0)))
and will then be unable to show that the agent can successfully traverese E2.
d) Would we be able to do the proof using only forward chaining?
ANSWER: Yes if all axioms and "theorems" in the proof above are in Horn form. If not, then MAYBE.
In the parts of the proof covered all clauses were Horn clauses, so there is hope. There is a technical
issue with the fact that the goal is not a single literal. This can be handled by adding a Horn clause:
Goal(v) and Loc(v, Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0))))
and Alive(Result(traverse(E3), Result(traverse(E1), Result(traverse(E1), S0)))) => QUERY_TRUE(v)
And then equivalently proving QUERY_TRUE(v) using forward chaining.
Deadline: Noon (12:00), Tuesday, December 9, 2014 ( strict deadline).
Submissions are to be solo.