CptS 540 Artificial Intelligence Homework 6 Solved

Description

General Instructions: Put your answers to the following problems into a PDF document and submit as an attachment under Content  Homework 6 for the course CptS 440 Pullman (all sections of CptS 440 and 540 are merged under the CptS 440 Pullman section) on the Blackboard Learn system by the above deadline. Note that you may submit multiple times, but we will only grade the most recent entry submitted before the deadline.

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}

1. There is a pit in location (3,1).
2. There is a breeze in the world, if and only if, there is a pit in the world.
3. If the agent and a live Wumpus are in the same location, then the agent is not alive.
4. There are at least two stenches in the world.
5. 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.

1. Wumpus(2,3)
2. x,y Pit(x,y)
3. t Action(Shoot,t)  a Arrow(a,t)
4. x,y,t₁,t₂ Agent(x,y,t₁)  Orientation(Right,t₁)  Action(TurnLeft,t₁)  (Agent(x,y,t₂)  Orientation(Up,t₂) )

3. Use resolution proof by refutation to prove the query below is true given the knowledge base.

Specifically,

1. Convert the knowledge base and negated query to CNF. Again, no need to show intermediate steps of the conversion. Give each clause a number.
2. 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),

1 and any necessary variable substitutions. Also be sure to conclude your proof with a statement of what was proven.

Knowledge Base:

• t₁,t₂ Orientation(Right,t₁)  Action(TurnLeft,t₁)  Inc(t₁,t₂)  Orientation(Up,t₂)
• t₁,t₂ Alive(Agent,t₁)  Action(GoForward,t₁)  Inc(t₁,t₂)  Alive(Agent,t₂)
• 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 <input_file>

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

2