This lecture is again about resolution. Recall that a resolution rule reads, "If we have a clause P, or V and, a clause ¬P or W, we may conclude a new clause V or W. " This is a sound method to prove that, a formula in conjunctive normal form is unsatisfiable. Note that we can only prove that the formula is unsatisfiable, or may be satisfiable, but we cannot answer other questions directly. But, sometimes by a simple transformation, we can do this. For instance; If we have to prove that some formula Phi is a tautology, that means it's always true. How to do that? Well, that's just equivalent to stating that ¬Phi is unsatisfiable. So, if we have a formula for which we have to prove that it's a tautology, just take an allegation of this formula, and apply the self-solver on it and, try to prove it by resolution. That's what a self-solver essentially does. If we have to prove that one formula implies another formula. Let's say, Phi implies Psi. Then we have to prove that Phi, and ¬Psi is unsatisfiable. So, the idea is to show that the property is not true. So, assume that Phi holds and Psi does ¬Hold, we have to derive a contradiction. So, if you can prove that Phi and ¬Psi is unsatisfiable, we can conclude that Phi implies Psi. To prove that two formulas, Phi and Psi are equivalent. Well, then Phi by implication, Psi should be a tautology. So, the negation of Phi by implication, Psi should be unsatisfiable. And it may be convenient to observe that this formula is logically equivalent to Phi or Psi and, ¬Phi or ¬Psi. Intuitively, this means if Phi and Psi are not equivalent then, one of them is false, and one of them is true. And that's exactly what this latter formula states. And if the formula is not in CNF, then first we have to apply a certain transformation as we will see later. Let's consider an example, and this is an example which is free after 'Lewis Carroll' the author of 'Alice in Wonderland' Has shown that good-natured-tenured professors are dynamic, grumpy-student advisers play slot machines and a lot of similar requirements, then we have to prove that no student adviser is smoking. How to treat such a problem? Well, the first step of course is give names to every notion to be formalized. Let's say good natured, we gave the name A, and the opposite of good natured, is grumpy. Tenured, we gave the name B. Professor,we gave the name C, and so on. And now we can transform our problem to, assume properties 1-12, exactly the requirements as given. And we have to conclude that no student adviser is smoking, and this formula stating that, ¬M and F should hold. And, as we just said, if we have to prove or implication, we simply assume that the assumptions hold and, the conclusions does ¬Hold. And from that we have to derive a contradiction. So, we have to prove that a formula consisting of the requirements, 1-12, and M, and F. This formula is unsatisfiable. Every property 1, 2, 3 and so on, can be written as a gross as follows; For instance, look at the first one: Good-natured, tenured professors are dynamic. And good-natured, we called A, tenured we called B, professor we called C, and dynamic we called D. So, this claim states that if A holds, if B holds and if C holds, then we can conclude to D. Stated in a formula that's, A and B and C, implies D and this is logically equivalent to the clause ¬A, or ¬B, or ¬C, or D. So, we have to prove that the following big formula is unsatisfiable. The conjunction of all of these 14 clauses. How to do that? Well, we will apply unit resolution. That means, if we have a unit clause in this case, M and F. If we have a clause M, we may remove every ¬M in the rest of the formula. And similar for removing ¬F and, if we do so and we remove the remaining M and F, the resulting formula is this formula. Already has become a little bit smaller, but observe by doing so, we introduced a new unit clause namely ¬L. So, now we can do unit resolution, or ¬L meaning that we may remove L from every other clause and, if we do so and remove the clause ¬L we get this formula. And again we see that a few new unit clauses have been created A and H. So, we can continue. No need to think about it, completely mechanically, we can continue, we may remove ¬A everywhere and, ¬H everywhere. And then we have this formula and again two new unit clauses have been created, B and K. So, doing the same for B and K, we get this formula. And now we have seven clauses remaining, but now there is no unit clause anymore. But we can do a resolution for instance, if we look at clause Five and seven, five reads, I or J. Seven reads, ¬I, or E. If we do a resolution on I, we get J or E. And now we have the clause J or E, but clause six reads, ¬J or E. If we do resolution on these two, we get the new clause, E or E, which can shortly be written as E. So, now by this resolution step we created a new unit clause and, now we can continue by unit resolution. Let's do so. The remaining formula only consists of these four clauses, and again a new unit clause has been created, on which we can do unit resolution and then, after a few steps we see that we can both derive G, and ¬G, and then by unit resolution on G, and ¬G, we derive the empty clause, and we have proved that the original formula was unsatisfiable. We saw that how tautology implications and equivalence, can be proved by proving unsatisfiability of a modified formula. And we applied this to solve a classical puzzle from Lewis Carroll. And the resolution strategy we apply here, we apply unit resolution as long as possible and, only do other resolution steps if no unit resolution is possible. Thank you.