Resolution in First-Order Logic Explained | AI Lecture 48

[00:00:10]okay so we meet for the last time this semester and you want to look at the resolution method for a fool okay so as I might have mentioned earlier it was a method which was introduced by Alan Robinson in 1965 and since then it has been used extensively in theorem proving so things like for example the proof for Fermat's Last Theorem had extensive support from programs which were based on resolution method eventually and it's a complete method for proving a theorem or proving something which uses only one rule of inference which is the resolution rule and it doesn't in any other axioms essentially now talking more generally about logic as we said that logic is basically a system in which you define the language and then define some rules of inference in that language define the meaning of sentences in that language and then talk about soundness and completeness and as you define more and more expressive languages so we have seen only one step here moved from professional logic to first-order logic in which we said that we can talk about variables and quantifiers over variables it was shown by gödel in his theorem which was called buddha's completeness theorem that first-order logic is sound and complete essentially which means you can always devise a first-order logic system which is sound and which is complete and by complete we mean anything which is entailed my set of statements can be derived using the machinery that we are building essentially it turns out that that fol is sound complete but it's only semi decidable and what this means is that in particular it the way it applies to fol is as follows that if you give a true statement or statement which is entailed to the system and ask the system to prove it then there exists a proof for that statement in that system essentially and you can always devise a strategy and you can imagine the strategy is something like breadth-first search that always you know find the nearest in for instance first and eventually you will go farther and farther away and eventually you will find the proof so you can always devise a strategy to for finding a proof but if you give a statement which is not true then the system will never hold because there is no proof and the system may never come out saying that there is no proof now in the case of propositional logic because we are only dealing with a countable a countable set of propositions and usually it is finite we can always say that at least for finite set of propositions we can always say that there is no proof because we can try all combinations and eventually say that there is no way that this can this statement can be true so even if it is false you can come out and say false in the case of first order logic we cannot come out and say that your statement is false you can only keep trying essentially which boils down to saying that your program can get into an infinite loop essentially and which is of course not surprising that we have written all of us have written programs which get into infinite loop of course most of our programs get into infinite loops in the imperative languages because we have written it a long long loop or wrong exit criteria in logic programming or Prolog we don't control the flow of execution we simply state what is to be done of course we do control it in the order in which we write statements because as we observed Prolog does depth-first search essentially top to down and and left to right which means that if you write statements in the wrong order it is possible that it could get it into get into a infinite loop but even if you write statements in the correct order if this if the statement that you are trying to prove is not true it can still get into an infinite loop essentially okay so today wheels will go back to this example that we saw and so on a B on VC and let's on table C and E supposing this is given to you this is a set of facts given to you and you want to show that there exists an X and there exists a Y such that on X Y and Ling X and not Ling boy this is the goal that you want to show to be true and that's the facts given to you now you can see that forward chaining backward chaining doesn't make sense here because in your door in your database or knowledge base there are no implication statements both power chaining and backward chaining move sort of allow you to move across implication statement so if here alpha implies beta then if you have alpha then you can say yes beta is there or if you have the gold beta you can say the GU alpha can be a goal but there are no implication statements here given the set of facts and we are asked to show this here so you can imagine that power training and backward chaining does not work at all this is Li so you must of course convince yourself that this statement is true and as human beings we might use one technique which is called looking at the different cases of proof by cases you could say take the case when X is a and Y is B or look at B so there are two cases that either B is green or B is not green if B is green then X is equal to B and Y is equal to C and B is on C and B is green and Y is not 3 if B is not green then you can say X equal to a and Y is equal to B and a is green and B is not green so whether B is green or whether B is not green you can show that in either of the two cases this statement is true and if you further say that this this is the only possibility that one of them is true then you can argue that yes this statement must be true essentially so this this statement which I slipped in between which is that if you argue that one only one of them is true is essentially a part of classical logic in classical logic every statement is either true or false and there is nothing in between so it's called the law of excluded middle essentially which some people object to because of statements like this if I can say that P or not P is true or Q or not Q is true this is a true statement why because of the law of excluded middle either P must be true or not P must be true so in which case this this runt is true and this is true and both are true since Q so I can shuffle this and write it is not P or Q or not Q or P and then which I can write as P implies Q or giving place P so this is true for any two statements P and Q whether they in any language first order or professional or higher order languages doesn't matter and if you treat the implication as implies in the causal sense then people have difficulty with such statements because this imagines that P stands for the earth is flat and Q stands for the moon is green then you are saying that there is a causal connection between these two things that the earth is flat and the moon is green that either the earth is flat implies that the moon is B all the fact that moon is mean implies that the earth is fact essentially now obviously there is no causal connection between these two statements you take any two statements P and Q and this statement is a tautology and so always true essentially so which is why sometimes logicians tend to distinguish between logics with capture causal relationships and we will not go into that but rather they would see that instead of reading it as an implication here you must read it like this so when you say P implies Q it's easier to read it as this without getting worked up about it it says that either P is false or Q is true that's all you're saying is easy but when we read this is an implication we have the sense of it being a causal relationship which is not really the case is usually okay now let's get back to the resolution method and before we do that we want to look at this algorithm called unification algorithm which is a very famous algorithm what unification algorithm does is that it takes two patterns we'll use a more generic term than formulas and tries to unify them which means rights to find the substitution which will make them the same essentially these patterns are made up of two kinds of things one that one is constant and one is variable and variable is something that you can substitute something for the other and constants are or atoms as some people call it cannot be substituted cannot be changed they have this thing so for the sake of simplicity we will adopt a slightly different notation supposing I have this statement man X or let's say not man X of mortal X now this statement which is in the mathematical language of logic has this particular notation that you have the predicate name or it could be the function name in some situations followed by brackets followed by the arguments and then predicates connected using logical connectives essentially so you have to distinguish between different kinds of things for the sake of this unification algorithm let's assume that we have a uniform notation and the notation in that notation what this will look like is that I will use all here and the notation uses the question mark is a thing for variable this is just for the sake of understanding this algorithm easily you can always about the algorithm to this notation but this is simply is easier to use because it is a very uniform list like notation which those of you who have used lists would be happier to look at essentially so I have moved the whole sign outside so the outermost connective is first and then the inner connective which is not here so not man is written like this so not so this whole thing from this packet to this packet is one expression or term if you will just call it a term or a list so from here to here is a list which is so the first one is always a connective the first element in the list is always a connective or a predicate name in this case so here predicate name is differentiated and you know connective is so the first thing is in this case it's a predicate named man here it's a connective here it is a connective so this has got these two arguments this whole thing is one thing and this won't even it's a list of three elements so everything is a list of some number of elements and the only thing we need to worry about is that either something is a constant or an atom as the list people say or it's available essentially so and the only the point about that is an atom can only matter match an atom so if I'm matching this with if I want to match this with man Socrates so what what am I trying to do I am trying to do something like resolution if you recall I have this clause and I have this close and I have something here and I have the negation of that thing here resolutions rule if you remember always first of all it works in clause form that that you must express things in CNF like form and then you have to look for something versus and it's negation of a positive literal and the negation negative literal and in some sense cancel it out essentially and from there you can derive mortal X's so which means of course I don't have to match this man hex which mortal with man Socrates which is what the unification algorithm will allow me to do it will tell me what values for X will make this two expressions the same in our case we have just called it as a list here so to match this with this of course the predicate name must be the same so we are just treating it as an atom here which means it can only match them another item which is the same as men not can only match north or can only match or it's only the variables which can match something else so let's assume that we have an arbitrary nested pattern which is expressed as a list of this kind and we want to write a general algorithm which will find a unifier for any two patterns or a substitution for those two patterns which will make it the same this substitution is called a unifier and that's the algorithm that we are looking for a unification algorithm so the algorithm is called let's say it's called unify so I will just sketch it here and you can fill in the details so let's say X Y and what this does is it so I will write it in the prologue like fashion this part it is sub unify XY so like we doing when we often we write a program we add a third parameter to make life simpler for us we have added an empty list and call this a uni sub unify and what this is going to be is the substitution so obviously when you call it when we call the so x and y are any any such list arbitrary list we start off by supplying an empty substitution it so now we are interested in this sub unify so X Y theta where theta is a substitution we are trying to build what is the substitution and substitution is a collection of variable value pair is essentially it says X equal to X should be substituted by this why should we substitute by this and so on which will make the two patterns the same essentially and this algorithm goes to a series of cases I'll just list out the salient ones here so obviously if x and y are the same whether they are adam or whether they are a list then you don't need to do anything they already unify this mystery so some of the main cases are follows so these are cases so I'll just write it as if so let's understand this to mean that X is available then calls another function call we're unified X my feet up so if one of them is a variable then it is a candidate for being substituted by something else and that this function where unify will do likewise if Y is a variable you can also call ver unify with Y X and theta somewhere so this order may not be the perfect order I am writing here if Adam X then if X is equal to Y X and theta is so if X is an atom if the argument that we are trying to unify so this is going to be a recursive program so this x and y initially will be such bigger patterns but eventually when we drill down into into the list at some point they will be either a variable or an atom so if it's a variable then we just call it call verifiably the other argument if it's an atom we check whether it is matching or not essentially so if it's not a variable and if it's not an atom it must be a list then we say if length x is not equal to length it's a list so we can compute its length return field if the two lists are of unequal length then you can never make them match else make recursive calls so make who I'll just write it like this okay appropriate recursive calls what does that mean that for example if this is one of my arguments and this is X and this X has a list of three elements the first element is this constant or the second element is this list which is this whole thing and the third element is this other list so if I have another list of three elements I can try to match that and then I will make recursive calls once with this with this then another with this and another so I will incremental e build a substitution so that leaves with us with the task of writing that we're unify which is really building the substitution okay I might have skipped order to small details it doesn't matter X so when you make a call to where unify we know that X is a variable the other thing could be a list or it could be something else so let's say this is available and yn theta we know that the first thing is a variable essentially we have to do a few checks so essentially what we really want to do is to say add we're equal to Y to my theta add one more substitution but before doing that I want to so what if what do I want to do I want to say return theta unions well equal to why I want to basically add one more substitution which is the call I'm making but is am I allowed to do that I have to do a couple of checks first first is if where is already equal to Y then you can just return theta you don't have to do anything else it could be the case for example I'm comparing well these are not variables in this case so it doesn't matter but it could be that they are the same variable then you just return theta then if we able of course they don't fail so the variable happens to occur in Y then you return fail so let me use an example to illustrate why this is needed and this example is from this book by charniak and make the mode which describes it in this notation so the example is as follows not sees X so let's say C stands for a predicate and the meaning of C's is that the first argument can see the second argument so for example I see you or things like that and this is a universally quantified statement it is saying that for all X let's assume that X is people X cannot see X which means one cannot see oneself is usually so let's assume that that's a true statement and I have a rule which and let's say I am doing forward chaining and the rule is as follows again I am writing it in this new notation where instead of writing the implication sign I will write an if here then the antecedent and then the consequent so instead of saying this implies that consequent I am writing it in this list like notation which Arnie I can make them what they use which is quite a nice notation to use easy to process so this tool says you know always worry about the number of brackets in this sort of a thing so what does this rule say it's a universally quantified statement how would you read it in English so feet is a function remember that in first order logic the arguments to predicates can only be terms in terms are either variables so that our constraints or function so feet of Z dysfunction so let's say feet of that stand for Z its feet so this is saying that if anyone cannot see their feet they should that exactly which may be a true statement now the question is said should should this rule and this these two rules can we apply forward chaining here to infer that everyone should do it not given these two facts right so let's see how that particular statement that we are talking about if variable occurs in Y then we can fill you comes to over this cube so we are trying to unify this with this remember modus ponens or modified modus ponens the antecedent should match now we will make recursive calls first you see that this is a list of two arguments then we will make two recursive calls one with the first argument then one with the second argument then the first our first call this is an atom and this matches this so that is fine so the first recursive call will work and it will not change theta at all the second recursive call has a list of three elements and this also has a list of three elements so that's fine first we'll make a call with CS and C's here if in the first call this case will come if if this is an atom and this is a same atom and then do nothing in the second call we will do this so our algorithm will say okay X is a variable so I can call Val unify with X and X and Z and then in the last statement which I will reach this I will say add X is equal to Z I am NOT writing the question marks here to theta so this will go into theta so this is saying that if you want to make these two patterns the same substitute for X the value Zed and you will have theta now you have XS already been put as did you so let so whether whether you do this here or whether you do this later both ways it works in fact the others other situation is if wave has a value in theta value let's call it Z in theta and then if a label already has a value in theta then call sub unify with that value so in this example we already have a value Z in theta X equal to Z so if we have not changed this X that Clause will kick in and we will call with xn so we so the regressive call that sub unify call in this line here would be with the value of Z so with Z then feet of Z essentially so lets us assume that we have already made this red which is this case where this is happening now you are trying to unify this X which is a variable with feet off so this has become Zed by now so let me put an arrow here and so that this becomes it because we have substituted X with Z now we are making a call of a variable Z with a list which is feet of Z which is a Y so this is X in this statement here sorry this is this is where in this statement and this is y and this statement says that if we're occurs in Y then return failed so in this example Z occurs in this pattern or list so the algorithm should return failures in that we cannot unify this is which is good for us because you know then otherwise all of us would never have to die so this doesn't apply and this particular Clause here is meant to catch exactly this kind of a thing is easily so you can never read if I said with feet of Z you know if you substitute feet of Z for Z then you'll have to substitute feet of that for this dead also and then there's air inside and there's air inside and they didn't say so no that doesn't make sense okay so this is a unification algorithm and what it returns is the theta which is the most general unifier which can make the two patterns the same so for example if I have a statement P X Y Z and another statement P X let's say a constant K then you can see that I can have one unifier which is X is equal to B and Z equal to e that's a unifier I am NOT saying that this algorithm will find this it's a unifier so that's one unifier and there's another unifier which is simply Z equal to H this unifier is more general than this unified because it does less amount of substitution I mean anything that this does this also does but there is something which just has to be this known which this does not look so this is called more general than this we loved going into details we will accept that there is a partial order of unifiers and there is something called the most general unifier which is called mgu and this algorithm essentially returns the most general unifier so again without going into details we just accept the fact that it is desirable to find the most general unifier and the reason for that is that you can make the most general inferences from which you can always derive more specific inference inferences using the universal instantiation rule essentially okay so yeah I'm afraid we don't have to go into details over that but it's basically it's a standard algorithm which is really popular and theorem proving and we use it all the time so let us address this problem let's see and how the resolution method will solve this problem so to convert to solve a problem with resolution method you have to convert it into clause form and a clause form is a form which looks like for as follows there is some number of Universal quantifiers X 1 X 2 X n then there is a set of clauses c1 and c2 and ce k such a formula such a form of a formula is clause form where each CI is d1 or the d2 or D are and each II I is equal to L I or negation of n time so of course the inside part you will recognize as a conjunctive normal form a set of clauses which are joined by an and and each Clause is basically a disjunction of some some things and each of those things is either a literal which means an atomic statement or the negation of an atomic statement so you push the negation side all the way inside and you have removed or thrown away exist initial quantifiers luckily in our example we don't really have existential quantifiers or at least you'll see in a moment that we don't have but we discussed earlier how to handle existential quantifiers by using this Coulomb functions in this column Constance and that can be done and then rearranging any formula into CNF is something that I'm sure you have studied how to do that and then you move the universal quantifiers outside and when they are together or outside you can just throw it away and use the implicit quantifier form which is what we are doing here so what is it so if you recall the deduction theorem that we had talked about earlier it said that to show that this follows from this you are equivalent ly showing that this and this and this and this and this entails this and if you want to use the resolution method you will recall that to use the resolution method you must take the conclusion and take its negation and add it as a clause to your system essentially so this is already in closed form all we need to do is to convert this into take its negation so what's the negation of that the negation of that if I put a negation sign outside here I will have to push the negation sign inside because I have to convert it into this closed form so this will become for all X for all Y not on XY or not mean X or mean y-yeah so once this negation goes inside then it'll go inside the ends and converted it to an or so remember we have to push that against inside to the innermost place so this will become not on this will become not green and this negation a negation will cancel then this will become green way so let me write this here on X Y or green X all right okay so this is one clause I hope I express it in the implicit quantifier form and those are the other things given to us which is on a B and on VC so let's forget on tables see that's not useful for us I mean you can write it but it doesn't help us green a and let's say this on table C is here anyway we don't really need that so we have this clauses and we want to what is it we want to show that can we derive the null Clause from this and we are going to use the unification algorithm along the way our example is so simple that we don't really have to use a very complicated recursive version it's very simply you can match it so let's just like this from this and this I substitute X equal to a and Y is equal to B I get green a or not being B because I have not stated the resolution step of the rule for first of the logic but you can see that it's very similar to modified modus ponens you do you apply the substitution and in the dissolvent you have the substitution already applied especially so because I am saying X equal to a and Y is equal to B then this becomes say this becomes B and I get this especially then from this and this I can get similarly green B or not we in see is that correct hmm this should be negation here right and this will not finish and this should be negative yeah so all three were long way so negation on X Y negation green X has seen in that orange thing there and green by essentially so what we get here is not green a and green B and not green B or green C so is it correct No then from this and this I can get not green V and from this one and this one if you can keep track of the arrows I can get green V and from this and this so just so repeat from our navy and that negative gold so remember this is a negative goal that we have added we get not green a or green B then from on BC and the negative Gold we get not Queen B or green C but here we have said not green C so when we resolve this with this we get not green B only this remains when you resolve this with this this is green a this is not renamed so you get green beat and then we have not green B or green B and from that you get the null closes so you can see that there is a simple proof using the resolution method and if you look at the proof carefully you can see that it's trying to in some sense say at the same time that if this formula is to be unsatisfiable if this whole set of formulas which means only this formula because this is accepted to be true this is the premises given to us if this is to be false then it entails that at the same time B must be green and we must not be green and that of course is a contradiction so as we discussed earlier the resolution method is like a proof by contradiction so if you remember when we talked about power chaining or backward chaining there is no way you can move from this set of data to this conclusion essentially the conclusion holds that one there exists a block on another block so that the block on top is green and the block below is not green it's it's not even intuitively clear but it is true but we cannot derive it using first forward chaining or backward chaining but in resolution methods there is a very simple small proof for doing it so in fact this procedure by Allen Robinson was a big breakthrough in logical reasoning automatic theorem proving and nowadays automatic theorem proving is done in many different places for many different applications especially and the heart of this is this resolution method recently which is a sound and complete method for first-order logic okay so I think we should stop here and with this we will end this pools I must say I enjoy teaching the class and I hope some of you at least enjoyed the course