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

- [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:- Prove by contradiction using resolution with refutation

¬ (P ∧ Q) ⊨ ¬ P ∨ ¬ Q - Prove by contradiction using resolution with refutation

¬ P ∨ ¬ Q ⊨ ¬ (P ∧ Q)

- Prove by contradiction using resolution with refutation
- [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).
- All houses have at least one bathroom.
- There is a house in Minneapolis which costs more than any other house.
- There is only one house in Minneapolis which is in the historical register.
- There is a pet in each house.
- Rich people have big houses.
- All big houses are expensive.
- All expensive houses are big.
- A house is expensive if it is big.
- Any small house costs less than any big house.
- There is only one house with a garden.

- [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.
- ∀ x G(x) ⇒ H(x)
- ∀ x H(x) ⇒ I(x)
- ∀ x H(x) ⇒ J(x,D)
- ∀ x I(x) ⇒ J(C,x)
- ∀ x ∀ y I(x) ⇒ ¬ J(x,y)

- [25 points]
You are given the following knowledge base:
- No one is both a vegetarian and a butcher.
- Everyone, except butchers, likes vegetarians.
- John is a vegetarian.

If you use python go to https://github.com/aimacode/aima-python/blob/master/intro.ipynb for instructions and links to the files you need. As always, look at https://github.com/aimacode/aima-python/blob/master/tests/test_logic.py for examples on how to use the code. The code (which includes examples) is at https://github.com/aimacode/aima-python/blob/master/logic.py.

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

- [15 points]
Create a propositional data base with the following clauses :
- (P ∧ Q) ⇒ R
- S ⇒ Z
- Z ⇒ P
- S
- S ⇒ U
- U ⇒ Q

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.

- [10 points] Unify the following expressions:
- Hates(x,C) with Hates(A,y)
- Hates(x,C) with Hates(A,B)
- Dog(x,C,x) with Dog(A,y,k)
- Dog(x,C,x) with Dog(A,y,B)
- Likes(x,y) with Likes(friend(John),y)
- Likes(friend(x),y) with Likes(x,z)
- Likes(friend(x),y) with Likes(w,z)
- Knows(John,x) with Knows(y,mother(y))
- Knows(x,friend(x)) with Knows(A,y)
- Knows(x,friend(x)) with Knows(A,x)

Department of Computer Science and Engineering. All rights reserved.

Changes and corrections are in red.