Description
1. Convert the following English statements to first-order logic using the following predicates.
• Breeze(x,y): there is a breeze in location (x,y)
• Pit(x,y): there is a pit in location (x,y)
• Stench(x,y): there is a stench in location (x,y)
• Wumpus(x,y): the Wumpus is in location (x,y)
• Agent(x,y): the agent is in location (x,y)
• Alive(o): the object o is alive, where o {Agent,Wumpus}
a. There is a pit in location (3,1).
b. There is a breeze in the world, if and only if, there is a pit in the world.
c. If the agent and a live Wumpus are in the same location, then the agent is not alive.
d. There are at least two stenches in the world.
e. There is a breeze in location (2,2) and a pit in location (2,3).
2. Convert the following first-order logic sentences to conjunctive normal form (CNF). There is
no need to show the intermediate steps.
a. Wumpus(2,3)
b. x,y Pit(x,y)
c. t Action(Shoot,t) a Arrow(a,t)
d. x,y,t1,t2 Agent(x,y,t1) Orientation(Right,t1) Action(TurnLeft,t1)
(Agent(x,y,t2) Orientation(Up,t2) )
3. Use resolution proof by refutation to prove the query below is true given the knowledge base.
Specifically,
a. Convert the knowledge base and negated query to CNF. Again, no need to show
intermediate steps of the conversion. Give each clause a number.
b. Show each resolution step by indicated the two clauses being resolved (be sure to use
unique variable names for each clause), the resulting clause (give it a new number),
2
and any necessary variable substitutions. Also be sure to conclude your proof with a
statement of what was proven.
Knowledge Base:
• t1,t2 Orientation(Right,t1) Action(TurnLeft,t1) Inc(t1,t2) Orientation(Up,t2)
• t1,t2 Alive(Agent,t1) Action(GoForward,t1) Inc(t1,t2) Alive(Agent,t2)
• t Action(TurnLeft,t) Action(GoForward,t)
• Alive(Agent,1)
• Orientation(Right,1)
• Action(TurnLeft,1)
• Inc(1,2)
• Inc(2,3)
Query: t Alive(Agent,t) Orientation(Up,t)
4. CptS 540 Students Only. Create an input file for the Vampire theorem prover that can be used
to solve Problem 3. You should run Vampire using the command:
vampire –avatar off
Include your input file and the Vampire output in the PDF document for your Homework 6
solution. You can download the Vampire theorem prover from https://vprover.github.io/.
There is a Linux binary available there or you can compile from source on other platforms. For
your reference, below is the Vampire input file for the “criminal(west)” proof demonstrated in
class.
fof(a1, axiom,
! [X,Y,Z] : ((american(X) & weapon(Y) & sells(X,Y,Z) & hostile(Z))
=> criminal(X))).
fof(a2, axiom,
enemy(nono,america)).
fof(a3, axiom,
? [X] : (owns(nono,X) & missle(X))).
fof(a4, axiom,
! [X] : ((missle(X) & owns(nono,X)) => sells(west,X,nono))).
fof(a5, axiom,
american(west)).
fof(a6, axiom,
! [X] : (missle(X) => weapon(X))).
fof(a7, axiom,
! [X] : (enemy(X,america) => hostile(X))).
fof(c1, conjecture, criminal(west)).
