重点CS 4365

【重点CS 4365】CS 4365 Artificial Intelligence
Spring 2021
Assignment 3: Knowledge Representation & Reasoning
Part I: Due electronically by Wednesday, April 7, 11:59 p.m.
Part II: Due electronically by Wednesday, April 14, 11:59 p.m.
Part I: Programming (100 points)
In this problem you will be implementing a theorem prover for a clause logic using the resolution
principle. Well-formed sentences in this logic are clauses. As mentioned in class, instead of using
the implicative form, we will be using the disjunctive form, since this form is more suitable for
automatic manipulation. The syntax of sentences in the clause logic is thus:
Clause → Literal ∨ . . . ∨ Literal
Literal → ?Atom | Atom
Atom → True | False | P | Q | . . .
We will regard two clauses as identical if they have the same literals. For example, q ∨ ?p ∨ q,
q ∨ ?p, and ?p ∨ q are equivalent for our purposes. For this reason, we adopt a standardized
representation of clauses, with duplicated literals always eliminated.
When modeling real domains, clauses are often written in the form:
Literal ∧ . . . ∧ Literal ? Literal
In this case, we need to transform the clauses such that they conform to the syntax of the clause
logic. This can always be done using the following simple rules:

  1. (p ? q) is equivalent to (?p ∨ q)
  2. (?(p ∨ q)) is equivalent to (?p ∧ ?q)
  3. (?(p ∧ q)) is equivalent to (?p ∨ ?q)
  4. ((p ∧ q) ∧ . . .) is equivalent to (p ∧ q ∧ . . .)
  5. ((p ∨ q) ∨ . . .) is equivalent to (p ∨ q ∨ . . .)
  6. (?(?p)) is equivalent to p
    The proof theory of the clause logic contains only the resolution rule:
    ?a ∨ l1 ∨ . . . ∨ ln,
    a ∨ L1 ∨ . . . ∨ Lm
    l1 ∨ . . . ∨ ln ∨ L1 ∨ . . . ∨ Lm
    If there are no literals l1, . . . ln and L1, . . . , Lm, the resolution rule has the form:
    1
    ?a, a
    False
    Remember that inference rules are used to generate new valid sentences, given that a set of old
    sentences are valid. For the clause logic this means that we can use the resolution rule to generate
    new valid clauses given a set of valid clauses. Consider a simple example where p ? q, z ? y and
    p are valid clauses. To prove that q is a valid clause we first need to rewrite the rules to disjunctive
    form: ?p ∨ q, ?z ∨ y and p. Resolution is then applied to the first and last clause, and we get:
    ?p ∨ q, p
    q
    If False can be deduced by resolution, the original set of clauses is inconsistent. When making
    proofs by contradiction this is exactly what we want to do. The approach is illustrated by the
    resolution principle explained below.
    The Resolution Principle
    To prove that a clause is valid using the resolution method, we attempt to show that the negation
    of the clause is unsatisfiable, meaning it cannot be true under any truth assignment. This is done
    using the following algorithm:
  7. Negate the clause and add each literal in the resulting conjunction of literals to the set of
    clauses already known to be valid.
  8. Find two clauses for which the resolution rule can be applied. Change the form of the
    produced clause to the standard form and add it to the set of valid clauses.
  9. Repeat 2 until False is produced, or until no new clauses can be produced. If no new clauses
    can be produced, report failure; the original clause is not valid. If False is produced, report
    success; the original clause is valid.
    Consider again our example. Assume we now want to prove that ?z ∨ y is valid. First, we
    negate the clause and get z ∧ ?y. Then each literal is added to the set of valid clauses (see 4. and
    5.). The resulting set of clauses is:
  10. ?p ∨ q
  11. ?z ∨ y
  12. p
  13. z
  14. ?y
    Resolution on 2. and 5. gives:
  15. ?p ∨ q
    2
  16. ?z ∨ y
  17. p
  18. z
  19. ?y
  20. ?z
    Finally, we apply the resolution rule on 4. and 6. which produces False. Thus, the original
    clause ?z ∨ y is valid.
    (A) The Program
    Files and Task Description
    Your program should take exactly one argument from the command line:
  21. A .kb file that contains the initial KB and the clause whose validity we want to test. The
    input file contains n lines organized as follows: the first n ? 1 lines describe the initial KB,
    while line n contains the (original) clause to test. Note that the KB is written in CNF, so
    each clause represents a disjunction of literals. The literals of each clause are separated by a
    blank space, while negated variables are prefixed by ~.
    Your program should adhere to the following policy:
    ? If the negated version of the clause to validate has ANDs, your program should split it into
    separate clauses. These clauses should be added to the KB from left to right order.
    ? Resolution should proceed as follows: For each clause i[1,n] (where n is the last clause in
    the KB), attempt to resolve clause i with every previous clause j[1,i) (in order). If a new
    clause is generated, it is added to the end of the KB (therefore the value of n changes). Your
    system should continue trying to resolve the next clause (i+1) with all previous clauses until
    1) a contradiction is found (in which case ’Contradiction’ should be added to the KB) or 2)
    all possible resolutions have been performed.
    ? Redundant generated clauses should not be added to the KB. A clause is redundant if the KB
    contains another clause which is logically equivalent to it.
    ? Clauses that evaluate to True should not be added to the KB.
    ? Generated clauses should not have redundant (repeated) literals.
    3
    Requirements: Output
    Your program should implement the resolution algorithm as explained in the previous section.
    Your program should output a line for every clause in the final KB (in the order they were added),
    each line should be single-space-separated and contain: 1) the clause number followed by a period
    (starting from 1), 2) the clause in DNF, and 3) the parent clauses (if this clause was generated
    through resolution) written as {i, j}. Finally, your program should print a final line containing the
    word Valid or Fail depending on whether the proof by contradiction succeeded or not.
    Let us consider a correct solution for testing the validity of ?z ∨ y, given the input:
    ~p q
    ~z y
    p
    ~z y
    Your program’s output should be:
  22. ~p q {}
  23. ~z y {}
  24. p {}
  25. z {}
  26. ~y {}
  27. q {3, 1}
  28. y {4, 2}
  29. ~z {5, 2}
  30. Contradiction {7, 5}
    Valid
    (B) Power Plant Diagnosis
    In the last part of this assignment you will be using your resolution prover to verify the safety
    requirements of a reactor unit in a nuclear power plant. The reactor unit is shown in the figure on
    the next page and consists of a reactor R, two heat exchangers H1 and H2, two steam valves V 1
    and V 2, and a control stick l for changing the level of energy production. The state of the reactor
    unit is given by 5 propositional variables l, okH1, okH2, V 1 and V 2. If l has the value True
    the production level is 2 energy units. Otherwise, the production level is 1 energy unit. At least
    one working heat exchanger is necessary for each energy unit produced to keep the reactor from
    overheating. Unfortunately a heat exchanger i can start leaking reactive water from the internal
    cooling system to the surroundings. okHi is False if heat exchanger Hi is leaking. Otherwise,
    okHi is True. When a heat exchanger i is leaking, it must be shut off by closing its valve V i. The
    state variable V i indicates whether the valve V i is closed (False) or open (True). Formally, the
    safety requirements are described by the following clauses:
    4
    NoLeak ∧ LowT emp ? ReactorUnitSafe
    NoLeakH1 ∧ NoLeakH2 ? NoLeak
    okH1 ? NoLeakH1
    ?okH1 ∧ ?V 1 ? NoLeakH1
    okH2 ? NoLeakH2
    ?okH2 ∧ ?V 2 ? NoLeakH2
    l ∧ V 1 ∧ V 2 ? LowT emp
    ?l ∧ V 1 ? LowT emp
    ?l ∧ V 2 ? LowT emp
    Assume that the current state of the reactor unit is given by the clauses:
    ?l
    ?okH2
    okH1
    V 1
    ?V 2
  31. Rewrite the safely rules from their implicative form to the disjunctive form used by your
    resolution prover. The initial set of valid clauses is the union of the rule clauses and the
    clauses defining the current state. Write the clauses in a file called facts.txt.
  32. Use your resolution prover to test whether LowT emp is a valid clause:
    (a) Save the input in a file called task1.in.
    (b) Test the result of your prover.
  33. Now test the validity of ReactorUnitSafe in a similar way:
    (a) Save the input in a file called task2.in.
    (b) Test the result of your prover.
  34. Consider a simpler set of safety rules:
    5
    NoLeakH1 ∧ NoLeakH2 ? NoLeak
    okH1 ? NoLeakH1
    ?okH1 ∧ ?V 1 ? NoLeakH1
    okH2 ? NoLeakH2
    ?okH2 ∧ ?V 2 ? NoLeakH2
    and a reduced current state description:
    ?okH2
    okH1
    ?V 2
    Test the validity of ?NoLeak:
    (a) Save the input in a file task3.in.
    (b) Test the result of your prover.
    Implementation and Submission Requirements
    The program must be written in C/C++, Java (JDK 8), or Python, and needs to be run/compile
    on the UTD Linux boxes without installing extra software.
    You may submit as many source files as needed, but you must make sure your provide a
    main code entry that follows the following naming convention:
    ? Java: Main.java
    ? Python: main.py
    ? C: main.c
    ? C++: main.cpp
    Your code should not use any external libraries.
    Submission
    You must directly submit all your source files, task 1, 2, and 3 .in files, and the facts.txt file
    to eLearning (do not put them in a folder or zip file). Any program that does not conform to
    this specification will receive no credit.
    Grading
    Make sure you follow the formatting from the example test files: be careful not to insert
    extra lines, tabs instead of spaces, etc ... When you submit, your code will be graded using
    hidden test cases, so we encourage you to test your code thoroughly.
    6
    Important: Be mindful of the efficiency of your implementation; as the test cases we will
    use are quite long, poorly written code might time out (and receive no credit!). We will
    provide you with example input files and approximate timings for each, so you can get an
    idea of how fast your code is.
    Part II: Written Problems (100 points)
  35. Representing Sentences in First-Order Logic (32 points)
    Assume that you are given the following predicates, where the universe of discourse consists
    of all the students in your class.
    I(x): x has an Internet connection
    C(x, y): x and y have chatted over the Internet
    Write the following statements using these predicates and any needed quantifiers.
    (a) Exactly one student in your class has an Internet connection.
    (b) Everyone except one student in your class has an Internet connection.
    (c) Everyone in your class with an Internet connection has chatted over the Internet with
    at least one other student in your class.
    (d) Someone in your class has an Internet connection but has not chatted with anyone else
    in your class.
    (e) There are two students in your class who have not chatted with each other over the
    Internet.
    (f) There is a student in your class who has chatted with everyone in your class over the
    Internet.
    (g) There are at least two students in your class who have not chatted with the same person
    in your class.
    (h) There are two students in the class who between them have chatted with everyone else
    in the class.
  36. Validity and Satisfiability (8 points)
    For each of the sentences below, decide whether it is valid, satisfiable, or neither. Verify your
    decisions using truth tables or the Boolean equivalence rules.
    (a) Big ∨ Dumb ∨ (Big ? Dumb)
    (b) (Smoke ? F ire) ? ((Smoke ∧ Heat) ? F ire)
  37. Models (12 points)
    Consider a world in which there are only four proposition, A, B, C, and D. How many
    models are there for the following sentences? Justify your answer.
    7
    (a) (A ∧ B) ∨ (B ∧ C)
    (b) A ∨ B
    (c) A ? B ? C
  38. Unification (12 points)
    Compute the most general unifier (mgu) for each of the following pairs of atomic sentences,
    or explain why no mgu exists. (Recall that lowercase letters denote variables, and uppercase
    letters denote constants.)
    (a) Q(y, Gee(A, B)), Q(Gee(x, x), y).
    (b) Older(F ather(y), y), Older(F ather(x), John).
    (c) Knows(F ather(y), y), Knows(x, x).
  39. Inference in First-Order Logic (36 points)
    Consider the following statements in English.
  40. Every child loves every candy.
  41. Anyone who loves some candy is not a nutrition fanatic.
  42. Anyone who eats any pumpkin is a nutrition fanatic.
  43. Anyone who buys any pumpkin either carves it or eats it.
  44. John buys a pumpkin.
  45. Lifesavers is a candy.
    Assume that you are given the following predicates:
    ? Child(x) — x is a child.
    ? F anatic(x) — x is a nutrition fanatic.
    ? Candy(y) — y is a candy.
    ? P umpkin(y) — y is a pumpkin.
    ? Carves(x, y) — x carves y.
    ? Eats(x, y) — x eats y.
    ? Buys(x, y) — x buys y.
    ? Loves(x, y) — x loves y.
    (a) (12 pts) Translate the six statements above into first-order logic using these predicates.
    (b) (12 pts) Convert the six sentences in part (a) into clausal form.
    (c) (12 pts) Prove using resolution by refutation that If John is a child, then John carves
    some pumpkin. Show any unifiers required for the resolution. Be sure to provide a
    clear numbering of the sentences in the knowledge base and indicate which sentences
    are involved in each step of the proof.

    推荐阅读