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 → Atom →
Literal ∨ . . . ∨ Literal ¬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)isequivalentto(¬p∨q)
2. (¬(p ∨ q)) is equivalent to (¬p ∧ ¬q)
3. (¬(p ∧ q)) is equivalent to (¬p ∨ ¬q)
4. ((p∧q)∧…)isequivalentto(p∧q∧…) 5. ((p∨q)∨…)isequivalentto(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:
1. Negate the clause and add each literal in the resulting conjunction of literals to the set of clauses already known to be valid.
2. 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.
3. 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:
1. ¬p∨q 2. ¬z ∨ y 3. p
4. z
5. ¬y
Resolution on 2. and 5. gives:
1. ¬p∨q
2
2. ¬z ∨ y 3. p
4. z
5. ¬y
6. ¬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:
1. 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: 1. ∼p q {}
2. ∼z y {}
3.p{}
4.z{}
5. ∼y{}
6. q {3, 1}
7. y {4, 2}
8. ∼z {5, 2}
6. 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∧LowTemp ⇒ NoLeakH1 ∧ NoLeakH2 ⇒ okH1 ⇒ ¬okH1∧¬V1 ⇒ okH2 ⇒ ¬okH2∧¬V2 ⇒ l∧V1∧V2 ⇒ ¬l∧V1 ⇒ ¬l∧V2 ⇒
ReactorUnitSafe N oLeak NoLeakH1 NoLeakH1 NoLeakH2 NoLeakH2 LowTemp LowTemp LowTemp
Assume that the current state of the reactor unit is given by the clauses:
¬l ¬okH2 okH1 V1 ¬V2
1. 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.
2. 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.
3. 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.
4. Consider a simpler set of safety rules:
5
Test the validity of ¬NoLeak:
(a) Save the input in a file task3.in.
(b) Test the result of your prover.
NoLeakH1 ∧ NoLeakH2 ⇒ okH1 ⇒ ¬okH1∧¬V1 ⇒ okH2 ⇒ ¬okH2∧¬V2 ⇒
N oLeak NoLeakH1 NoLeakH1 NoLeakH2 NoLeakH2
and a reduced current state description:
¬okH2 okH1 ¬V2
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)
1. 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.
2. 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) 3. 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
4. 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(Father(y),y),Older(Father(x),John). (c) Knows(Father(y),y),Knows(x,x).
5. Inference in First-Order Logic (36 points) Consider the following statements in English.
1. Every child loves every candy.
2. Anyone who loves some candy is not a nutrition fanatic. 3. Anyone who eats any pumpkin is a nutrition fanatic.
4. Anyone who buys any pumpkin either carves it or eats it. 5. John buys a pumpkin.
6. 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)—xeatsy.
• Buys(x,y)—xbuysy.
• 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.
8