” CS 4365语言程序 写作、 辅导C/C++编程CS 4365 Artificial IntelligenceSpring 2021Assignment 3: Knowledge Representation ReasoningPart 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 resolutionprinciple. Well-formed sentences in this logic are clauses. As mentioned in class, instead of usingthe implicative form, we will be using the disjunctive form, since this form is more suitable forautomatic manipulation. The syntax of sentences in the clause logic is thus:Clause Literal . . . LiteralLiteral Atom | AtomAtom 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 standardizedrepresentation of clauses, with duplicated literals always eliminated.When modeling real domains, clauses are often written in the form:Literal . . . Literal LiteralIn this case, we need to transform the clauses such that they conform to the syntax of the clauselogic. 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 pThe proof theory of the clause logic contains only the resolution rule:a l1 . . . ln,a L1 . . . Lml1 . . . ln L1 . . . LmIf there are no literals l1, . . . ln and L1, . . . , Lm, the resolution rule has the form:1a, aFalseRemember that inference rules are used to generate new valid sentences, given that a set of oldsentences are valid. For the clause logic this means that we can use the resolution rule to generatenew valid clauses given a set of Valid clauses. Consider a simple example where p q, z y andp are valid clauses. To prove that q is a valid clause we first need to rewrite the rules to disjunctiveform: p q, z y and p. Resolution is then applied to the first and last clause, and we get:p q, pqIf False can be deduced by resolution, the original set of clauses is inconsistent. When makingproofs by contradiction this is exactly what we want to do. The approach is illustrated by theresolution principle explained below.The Resolution PrincipleTo prove that a clause is valid using the resolution method, we attempt to show that the negationof the clause is unsatisfiable, meaning it cannot be true under any truth assignment. This is doneusing the following algorithm:1. Negate the clause and add each literal in the resulting conjunction of literals to the set ofclauses already known to be valid.2. Find two clauses for which the resolution rule can be applied. Change the form of theproduced 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 clausescan be produced, report failure; the original clause is not valid. If False is produced, reportsuccess; the original clause is valid.Consider again our example. Assume we now want to prove that z y is valid. First, wenegate the clause and get z y. Then each literal is added to the set of valid clauses (see 4. and5.). The resulting set of clauses is:1. p q2. z y3. p4. z5. yResolution on 2. and 5. Gives:1. p q22. z y3. p4. z5. y6. zFinally, we apply the resolution rule on 4. and 6. which produces False. Thus, the originalclause z y is valid.(A) The ProgramFiles and Task DescriptionYour 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. Theinput 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, soeach clause represents a disjunction of literals. The literals of each clause are separated by ablank 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 intoseparate 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 inthe KB), attempt to resolve clause i with every previous clause j[1,i) (in order). If a newclause is generated, it is added to the end of the KB (therefore the value of n changes). Yoursystem should continue trying to resolve the next clause (i+1) with all previous clauses until1) 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 KBcontains 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.3Requirements: OutputYour 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 generatedthrough resolution) written as {i, j}. Finally, your program should print a final line containing theword 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 qz ypz yYour programs 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 DiagnosisIn the last part of this assignment you will be using your resolution prover to verify the safetyrequirements of a reactor unit in a nuclear power plant. The reactor unit is shown in the figure onthe next page and consists of a reactor R, two heat exchangers H1 and H2, two steam valves V 1and V 2, and a control stick l for changing the level of energy production. The state of the reactorunit is given by 5 propositional variables l, okH1, okH2, V 1 and V 2. If l has the value Truethe production level is 2 energy units. Otherwise, the production level is 1 energy unit. At leastone working heat exchanger is Necessary for each energy unit produced to keep the reactor fromoverheating. Unfortunately a heat exchanger i can start leaking reactive water from the internalcooling 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. Thestate variable V i indicates whether the valve V i is closed (False) or open (True). Formally, thesafety requirements are described by the following clauses:4NoLeak LowT emp ReactorUnitSafeNoLeakH1 NoLeakH2 NoLeakokH1 NoLeakH1okH1 V 1 NoLeakH1okH2 NoLeakH2okH2 V 2 NoLeakH2l V 1 V 2 LowT empl V 1 LowT empl V 2 LowT empAssume that the current state of the reactor unit is given by the clauses:lokH2okH1V 1V 21. Rewrite the safely rules from their implicative form to the disjunctive form used by yourresolution prover. The initial set of valid clauses is the union of the rule clauses and theclauses 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:5NoLeakH1 NoLeakH2 NoLeakokH1 NoLeakH1okH1 V 1 NoLeakH1okH2 NoLeakH2okH2 V 2 NoLeakH2and a reduced current state description:okH2okH1V 2Test the validity of NoLeak:(a) Save the input in a file task3.in.(b) Test the result of your prover.Implementation and Submission RequirementsThe program must be written in C/C++, Java (JDK 8), or Python, and needs to be run/compileon the UTD Linux boxes without installing extra software.You may submit as many source files as needed, but you must make sure your provide amain code entry that follows the following naming convention: Java: Main.java Python: main.py C: main.c C++: main.cppYour code should not use any external libraries.SubmissionYou must directly submit all your source files, task 1, 2, and 3 .in files, and the facts.txt fileto eLearning (do not put them in a folder or zip file). Any program that does not conform tothis specification will receive no credit.GradingMake sure you follow the Formatting from the example test files: be careful not to insertextra lines, tabs instead of spaces, etc … When you submit, your code will be graded usinghidden test cases, so we encourage you to test your code thoroughly.6Important: Be mindful of the efficiency of your implementation; as the test cases we willuse are quite long, poorly written code might time out (and receive no credit!). We willprovide you with example input files and approximate timings for each, so you can get anidea 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 consistsof all the students in your class.I(x): x has an Internet connectionC(x, y): x and y have chatted over the InternetWrite 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 withat least one other student in your class.(d) Someone in your class has an Internet connection but has not chatted with anyone elsein your class.(e) There are two students in your class who have not chatted with each other over theInternet.(f) There is a student in your class who has chatted with everyone in your class over theInternet.(g) There are at least two students in your class who have not chatted with the same personin your class.(h) There are two students in the class who between them have chatted with everyone elsein the class.2. Validity and Satisfiability (8 points)For each of the sentences below, decide whether it is valid, satisfiable, or neither. Verify yourdecisions 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 manymodels are there for the following sentences? Justify your answer.7(a) (A B) (B C)(b) A B(c) A B C4. 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 uppercaseletters 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 carvessome pumpkin. Show any unifiers required for the resolution. Be sure to provide aclear numbering of the sentences in The knowledge base and indicate which sentencesare involved in each step of the proof.请加QQ：99515681 或邮箱：99515681@qq.com WX：codehelp
“
添加老师微信回复‘’官网 辅导‘’获取专业老师帮助，或点击联系老师1对1在线指导。
