Homework 6 Solution

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 above deadline.

    1. Consider the following logic problem:

All people who like computers also like coding.
All people who like coding and like chess will learn AI.
For all people that learn AI, there is at least one company that will hire them. All people who are hired by some company will be rich and famous.

        a. We will solve this problem using first-order logic. First, show one first-order logic sentence for each of the first four sentences in the above problem. You may only draw from the following first-order predicates.
            ▪ Like(x, Chess)
            ▪ Like(x, Computers)
            ▪ Like(x, Coding)
            ▪ Learn(x, AI)
            ▪ Hire(x, y) – which means company x hires person y
            ▪ Rich(x)
            ▪ Famous(x)



        b. Convert each of the four sentences from part (a) into Conjunctive Normal Form (CNF). You may just show the final result for each sentence; no need to show the intermediate steps. Number each clause. We will refer to these clauses as the knowledge base (KB) below.




        c. To the KB from part (b), add the two facts: “Larry likes computers” and “Larry likes chess”. Using this augmented KB, perform a resolution proof by refutation to prove “Rich(Larry)”. In your proof, be sure to do the following:
            ▪ For each resolution step, show the numbers of the two clauses used, the resulting clause, any variable substitutions resulting from unifying the complementary literals, and then number the resulting clause.
            ▪ Be sure to use unique variables (e.g., x1, x2, y1, etc.) for each use of a clause from the KB.
            ▪ Remember: each resolution step can only be done with two clauses at a time and can eliminate only one literal from each clause.



        d. To the KB from part (b), add the fact: “There exists someone who learns AI.” Be sure to first convert this fact to CNF. Using this augmented KB, perform a resolution proof by refutation to prove “x Famous(x)”, following the guidelines in part (c).


    2. CptS 540 Students Only. Create an input file for the Vampire theorem prover that can be used to solve Problem 1c. Include your input file and the Vampire output in your Homework 6 submission. You can include them as separate text files or cut-and-paste them into the document containing the rest of your solution. You can download the Vampire theorem prover from https://vprover.github.io/. There is a Linux binary available there that runs on the ssh1- ssh10 servers that all grad students have access to. You can run it on your own machine if you prefer or build it from source. For your reference, below is the Vampire input file for the “criminal(west)” proof demonstrated in class.