Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due
ECE 598HZ: Advanced Topics in Machine Learning and Formal Methods Fall 2024
Your name, netid Homework 3
Due Dec 9th 11:59pm
Typeset your solutions using LATEX zip your solutions in a single file called netid-598-F24.zip and upload this file through Canvas.
Start working on your homework EARLY!
Problem 1: Resolution Refutation for Propositional Logic (40 pts)
A chemical processing plant has implemented a multi-layered safety system with the following protocols:
1. If both the pressure is high AND the temperature sensor is working, then either the emergency valve must be opened OR the backup cooling system activates.
2. If toxic gas is detected AND the ventilation system is working, then the emergency valve must be opened.
3. When the emergency valve opens OR the backup cooling activates, the safety alarm must sound.
4. Both the temperature sensor and ventilation system are confirmed to be working.
Currently, the pressure is high and toxic gas has been detected. (this can be seen as an additional premise).
Given the 5 premises above, the goal is to prove that the alarm will sound using refutation resolution. First, let’s define our propositional variables as:
1. P: Pressure is high
2. E: Emergency valve is opened
3. B: Backup cooling is activated
4. V: Ventilation system is working
5. T: Temperature sensor is working
6. G: Toxic gas is detected
7. A: The alarm sounds
Then answer the following question:
11. Write all five premises and the goal to prove using the propositional variables above. (10 pts)
2. Convert all premises into Conjunctive Normal Form (5 pts)
3. Negate the goal, and apply resolution refutation to prove that the alarm will sound. Show each resolution step clearly. (20 pts)
4. Draw a resolution tree to illustrate your proof. (5 pts)
5. If the temperature sensor is not working, can you still prove that the alarm will sound? (Extra 10 pts)
Problem 2: Natural Number Games with Lean (60 pts)
Learn the Lean theorem prover with a set of nicely designed games available at: https://adam.math.hhu.de/#/g/leanprover-community/nng4
1. Complete the “Level 8 / 8 : 2+2=4” in “Tutorial World”. Submit a screenshot for completion, and your program as a text file proof1.lean (15 pts)
2. Complete the “Level 5 / 5 : add right comm” in “Addition World”. Submit a screenshot for completion, and your program as a text file proof2.lean. (15 pts)
3. Complete the “Level 11 / 11 : 2 + 2 = 5” in “Implication World”. Submit a screenshot for completion, and your program as a text file proof3.lean. (15 pts)
4. Complete the “Level 6 / 6 : add left eq zero” in “Advanced Addition World”. Submit a screenshot for completion, and your program as a text file proof4.lean. (15 pts)
5. Complete the “Level 7 / 9 : An algorithm for equality” in “Algorithm World”. Submit a screenshot for completion, and your program as a text file proof5.lean. (Extra 20 pts)
Submission instructions
In your report, add a screenshot showing that you solved each level in Editor mode. You can toggle the “Editor mode” by clicking the </> button on the top-right of the webpage. An example is given below. In addition, copy your code in editor mode and submit it as a text file with the filename specified above.
Figure 1: You should show your complete code in the “Editor mode” in your submission. The editor mode is demonstrated in the figure above, where you can directly copy all lines of code you wrote to solve each level. Copy your code into a text file (e.g., the 5 lines of code in the figure) as specified in each question. In addition, submit a screenshot like above with your full program in
Editor mode and the message “Level completed”.