CptS440-540 Homework 6 Solved

General Instructions: Put your answers to the following problems into a PDF document and upload the document as your submission for 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 Canvas 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 first-order logic sentence into conjunctive normal form (CNF). There is no need to show intermediate steps.

   “x Stench(x) Þ $y Adjacent(x,y) Ù At(Wumpus,y)

2. Convert each of the following English statements into a single first-order logic sentence using the following constants and predicates.

• Constants: Apples, Oranges, Chess, Go, John, Mary. • Predicates:

o Likes(x,y): person x likes food y o Plays(x,y): person x plays game y

1. If a person likes Apples, then they play Chess.
2. If a person likes Oranges, then they play Go.
3. A person likes Apples or Oranges, but not both.
4. John likes Apples.
5. Mary does not like anything that John likes.

3. Convert each of the first-order logic sentences in Problem 2 to conjunctive normal form (CNF). There is no need to show intermediate steps. Assign each clause a number: C1, C2, etc.
4. Using the clauses from Problem 3, perform a resolution proof by refutation to prove the query “Plays(Mary,Go)”. Specifically,
   1. Show the clause corresponding to the negation of the query and assign it a number.
   2. Show each resolution step by indicated the two clauses being resolved (be sure to

      standardize the variables), the resulting clause (assign it a new number), and any necessary variable substitutions. Conclude your proof with a statement of what was proven.

Continued on next page…

1

5. CptS 540 Students Only. Create an input file for the Vampire theorem prover that can be used to solve Problem 4. Include your input file and the corresponding 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. Note that Vampire uses uppercase to denote variables, and lowercase for everything else, which is opposite from the textbook and Problems 1-4 above.

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