attatched file
Programming Assignment - III Theorem Proving by Resolution 4365 Artificial Intelligence 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. 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: We will regard two clauses as identical if they have the same literals. For example, ?? ⋁ ¬?? ⋁ ??, ?? ⋁ ¬??, and ¬?? ⋁ ?? are all 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: 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: (?? ⇒ ??) is equivalent to (¬?? ⋁ ??) (¬(?? ⋁ ??)) is equivalent to (¬?? ⋀ ¬??) (¬(?? ⋀ ??)) is equivalent to (¬?? ⋁ ¬??) ((?? ⋀ ??) ⋀ . . . ) is equivalent to (?? ⋀ ?? ⋀ . . . ) ((?? ⋁ ??) ⋁ . . . ) is equivalent to (?? ⋁ ?? ⋁ . . . ) (¬(¬??)) is equivalent to ?? The proof theory of the clause logic contains only the resolution rule: If there are no literals ??1, . . . ???? and ??1, . . . , ????, the resolution rule has the form: 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 ?? ⇒ ??, ?? ⇒ ?? and ?? are valid clauses. To prove that ?? is a valid clause we first need to rewrite the rules to disjunctive form: ¬?? ⋁ ??, ¬?? ⋁ ?? and ??. Resolution is then applied to the first and last clause, and we get: 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 ¬?? ⋁ ?? is valid. First, we negate the clause and get ?? ⋀ ¬??. Then each literal is added to the set of valid clauses (see 4. And 5.). The resulting set of clauses is: Resolution on 2. and 5. gives: Finally, we apply the resolution rule on 4. and 6. which produces False. Thus, the original clause ¬?? ⋁ ?? is valid. The Program Files and Task Description Your program should take exactly one argument from the command line: The path to 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 ?? − 1 lines describe the initial KB, while line ?? 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 ??[1, ??] (where n is the last clause in the KB), attempt to resolve clause ?? with every previous clause ??[1, ??) (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 (?? + 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. 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 {??, ??}. 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 ¬?? ⋁ ??, given the input: Your program’s output should be: 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 and consists of a reactor R, two heat exchangers ??1 and ??2, two steam valves ?? 1 and ?? 2, and a control stick ?? for changing the level of energy production. The state of the reactor unit is given by 5 propositional variables ??, ??????1, ??????2, ?? 1 and ?? 2. If ?? 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 ?? can start leaking reactive water from the internal cooling system to the surroundings. ???????? is False if heat exchanger ???? is leaking. Otherwise, ???????? is True. When a heat exchanger ?? is leaking, it must be shut off by closing its valve ?? ??. The state variable ?? ?? indicates whether the valve ?? ?? is closed (False) or open (True). Formally, the safety requirements are described by the following clauses: Assume that the current state of the reactor unit is given by the clauses: 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 ?????????????? is a valid clause: a. Save the input in a file called task1.in. b. Save the result of your prover in the file task1.out. 3. Now test the validity of ?????????????????????????????? in a similar way: a. Save the input in a file called task2.in. b. Save the result of your prover in the file task2.out. 4. Consider a simpler set of safety rules: and a reduced current state description: Test the validity of ¬????????????: a. Save the input in a file task3.in. b. Save the result of your prover in the file task3.out. Implementation and Submission Requirements The program must be written in C++ (g++ 7.5.0), Java (openjdk 11.0.13 2021-10-19), or Python (3.6.9). You may submit as many source files as needed, but you must make sure you provide a main code is in a single file and it uses the following naming convention. Specifically, if you are using: • Python - Make sure that your primary source file is main.py and that your code runs successfully after executing python main.py
. • C++ - Make sure that your primary source file is main.cpp and that your code runs successfully after executing g++ main.cpp -o a.out -std=c++17 and ./a.out . • Java - Make sure that your primary source file is Main.java and that your code runs successfully after executing javac Main.java and java Main. Your code should not use any external libraries. If it does, the autograder will not be able to run your code and you will receive no credit. Submission Directly submit all your source files, task1.in, task2.in, task3.in and the facts.txt file to the submission link in eLearning. Do not create any folder and do not rename the files or upload the files in a zip file or folder (your homework will not be graded otherwise). Power Plant Diagnosis Implementation and Submission Requirements