CSci 4511 - Homework 3

Homework 3 -- due date postponed to Thursday March 22

This homework will be graded out of 100 points. It will count 5% of the grade. You can submit the homework with no late penalty up to Sunday March 19.

Written questions

  1. [30 points] Decide if the following sentences are valid, unsatisfiable, or neither. To do it, use the truth tables and equivalency rules in Chapter 7.
    1. Big ⇒ Big
    2. Big ⇒ Heavy
    3. (Big ⇒ Heavy) ⇒ (¬ Big ⇒ ¬ Heavy)
    4. Big ∨ Heavy ∨ ¬ Heavy
    5. ((Big ∧ Dense)⇒ Heavy) ⇔ ((Big ⇒ Dense) ∨ (Heavy ⇒ Dense))
    6. (Big ⇒ Dense) ⇒ ((Big ∧ Heavy) ⇒ Dense)
    7. Small ∨ Cute ∨ (Small ⇒ Cute)
    8. (Small ∧ Cute) ∨ ¬ Cute
    9. ((Rain ⇒ Wet) ∧ (Wet ⇒ Cold)) ⇒ (Rain ⇒ Cold)
    10. ((Rain ∨ Wet ) ∧ ( ¬ Wet ∨ Cold)) ⇒ ( Rain ∨ Cold )
  2. [15 points] For each of the following formulas, state briefly if it is a correct representation in propositional calculus of the sentence "If Bill works and his father stays at home, then his mother is happy" or not and explain why. The propositions used in the sentences should have an obvious interpretation.
    1. BillWork ∧ DadHome ∧ MomHappy
    2. (BillWork ∧ DadHome) ⇒ MomHappy
    3. (BillWork ∨ DadHome) ⇒ MomHappy
    4. MomHappy ⇒ (BillWork ∧ DadHome)
    5. ¬ BillWork ∨ (¬ MomHappy ∨ DadHome)
  3. [25 points] Convert the following set of propositional clauses to CNF
    1. Cold ∧ Dry ⇒ Pleasant
    2. January ⇒ Winter ∧ Wet
    3. Winter ⇒ Dry
    4. Wet ⇒ Cold
    5. January
    and prove by resolution with refutation that it is Pleasant.

Programming questions

You need to submit the source files and the output obtained.

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: 

(load "aima.lisp")
(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.

To do resolution using the software, you first have to create a database, which in this case has to be propositional: (setq kb (make-prop-kb))
Use tell to add the knowledge, and ask to ask the question. Examples are in the logic test file.

  1. [10 points] Create a propositional data base, include in it the clauses from problem 3 above and prove it is Pleasant using the program.
  2. [10 points] Create a propositional data base and represent the following: "If the unicorn is mythical, then it is immortal but if it is not mythical then it is a mortal mammal. If the unicorn is either immortal or a mammal, then it is horned. The unicorn is magical, if it is horned."
  3. [10 points] Use ask to answer the following questions from the data base you created for the previous question:
    1. is the unicorn mythical?
    2. is the unicorn magical?
    3. is the unicorn horned?
    What can you say from the answers you get? Do the statements logically follow from the knowledge base? or not?
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.