CSci 4511 - Homework 4

Homework 4 -- due Thursday March 29

This homework will be graded out of 100 points. It will count 5% of the grade.
To avoid confusion, when you need to use resolution I added "with refutation".

Written questions

  1. [10 points] Two sentences in propositional calculus can be shown to be equivalent by proving that one entails the other and viceversa.
    Show that ¬ (P ∧ Q) ≡ ¬ P ∨ ¬ Q by doing the following steps:
    1. Prove by contradiction using resolution with refutation
      ¬ (P ∧ Q) ⊨ ¬ P ∨ ¬ Q
    2. Prove by contradiction using resolution with refutation
      ¬ P ∨ ¬ Q ⊨ ¬ (P ∧ Q)
  2. [25 points] Write each of the following sentences, in predicate calculus. Use the same predicates across the sentences. Use predicates such as House(x), Pet(x), In(x,y), Live(x,y), Big(x), and Cost(x,y).
    1. All houses have at least one bathroom.
    2. There is a house in Minneapolis which costs more than any other house.
    3. There is only one house in Minneapolis which is in the historical register.
    4. There is a pet in each house.
    5. Rich people have big houses.
    6. All big houses are expensive.
    7. All expensive houses are big.
    8. A house is expensive if it is big.
    9. Any small house costs less than any big house.
    10. There is only one house with a garden.
  3. [15 points] Transform to CNF the following knowledge base, where upper case arguments are constants, lower case arguments are variables. Do not forget to standardize variables apart.
    1. ∀ x G(x) ⇒ H(x)
    2. ∀ x H(x) ⇒ I(x)
    3. ∀ x H(x) ⇒ J(x,D)
    4. ∀ x I(x) ⇒ J(C,x)
    5. ∀ x ∀ y I(x) ⇒ ¬ J(x,y)
    Prove by resolution with refutation "¬ G(B)".
  4. [25 points] You are given the following knowledge base:
    1. No one is both a vegetarian and a butcher.
    2. Everyone, except butchers, likes vegetarians.
    3. John is a vegetarian.
    Write the sentences in predicate calculus, transform them to CNF, and use resolution with refutation to answer the question "Is there someone that John likes?".

Programming questions

You need to submit the output obtained.

If you use python go to for instructions and links to the files you need. As always, look at for examples on how to use the code. The code (which includes examples) is at

If you use Lisp do:

(aima-load 'all)
(aima-compile)   ; only the first time.  Do (aima-load 'logic) afterward
(test 'logic)    ; tests the functions in the logic package
Read the file logic/test-logic.lisp to see examples of how to call the functions you will need to use. Look in particular at how to write the logical connectors in the expressions.

  1. [15 points] Create a propositional data base with the following clauses :
    1. (P ∧ Q) ⇒ R
    2. S ⇒ Z
    3. Z ⇒ P
    4. S
    5. S ⇒ U
    6. U ⇒ Q
    Prove "R" using resolution with refutation. Remember that there is a function in the software to convert to CNF and a function to do resolution in propositional calculus.

    Then create a definite clause knowledge base (in python, use PropDefiniteKB(), in Lisp use (make-horn-kb)). Add to it the same clauses as before (they are all Horn clauses -- disjunction of literals with at most one positive literal). Use forward chaining (in python pl_fc_entails, in Lisp this function does not exist) to prove "R". In python the function you need is pl_fc_entails. In Lisp the function does not exist, so if you use Lisp skip this part.

  2. [10 points] Unify the following expressions:
    1. Hates(x,C) with Hates(A,y)
    2. Hates(x,C) with Hates(A,B)
    3. Dog(x,C,x) with Dog(A,y,k)
    4. Dog(x,C,x) with Dog(A,y,B)
    5. Likes(x,y) with Likes(friend(John),y)
    6. Likes(friend(x),y) with Likes(x,z)
    7. Likes(friend(x),y) with Likes(w,z)
    8. Knows(John,x) with Knows(y,mother(y))
    9. Knows(x,friend(x)) with Knows(A,y)
    10. Knows(x,friend(x)) with Knows(A,x)
Copyright: © 2018 by the Regents of the University of Minnesota
Department of Computer Science and Engineering. All rights reserved.
Comments to: Maria Gini
Changes and corrections are in red.