首页 >
> 详细

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:

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 ∧ 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

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

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)

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(F ather(y), y), Older(F ather(x), John).

(c) Knows(F ather(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) — 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.

联系我们

- QQ：99515681
- 邮箱：99515681@qq.com
- 工作时间：8:00-23:00
- 微信：codinghelp2

- Cs2461-10实验程序代做、代写java，C/C++，Python编程设 2021-03-02
- 代写program程序语言、代做python，C++课程程序、代写java编 2021-03-02
- Programming课程代做、代写c++程序语言、Algorithms编程 2021-03-02
- 代写csc1-Ua程序、代做java编程设计、Java实验编程代做 代做留学 2021-03-02
- 代做program编程语言、代写python程序、代做python设计编程 2021-03-02
- 代写data编程设计、代做python语言程序、Python课程编程代写 代 2021-03-02
- Cse 13S程序实验代做、代写c++编程、C/C++程序语言调试 代写留学 2021-03-02
- Mat136h5编程代做、C/C++程序调试、Python，Java编程设计 2021-03-01
- 代写ee425x实验编程、代做python，C++，Java程序设计 帮做c 2021-03-01
- Cscc11程序课程代做、代写python程序设计、Python编程调试 代 2021-03-01
- 代写program编程、Python语言程序调试、Python编程设计代写 2021-03-01
- 代做r语言编程|代做database|代做留学生p... 2021-03-01
- Data Structures代写、代做r编程课程、代做r程序实验 帮做ha 2021-03-01
- 代做data留学生编程、C++，Python语言代写、Java程序代做 代写 2021-03-01
- 代写aps 105编程实验、C/C++程序语言代做 代写r语言程序|代写py 2021-03-01
- Fre6831 Computational Finance 2021-02-28
- Sta141b Assignment 5 Interactive Visu... 2021-02-28
- Eecs2011a-F20 2021-02-28
- Comp-251 Final Asssessment 2021-02-28
- 代写cs1027课程程序、代做java编程语言、代写java留学生编程帮做h 2021-02-28