|
|
@@ -0,0 +1,92 @@
|
|
|
+# AI - lesson 08
|
|
|
+#### Francesco Arrigoni
|
|
|
+###### 2 December 2015
|
|
|
+## First Order Logic
|
|
|
+
|
|
|
+### Inference prodecures for first order logic
|
|
|
+
|
|
|
+- __substitution__ $\theta = \{variable / ground term\}$
|
|
|
+
|
|
|
+- __unification__ $UNIFY(\alpha,\beta)=\theta \alpha\theta=\beta\theta$
|
|
|
+
|
|
|
+|$\alpha$|$\beta$|$\theta|
|
|
|
+|---|---|---|
|
|
|
+|knows(John,x)|knows(John,Jane)|{x|Jane\}|
|
|
|
+|knows(John,x)|knows(y,oj)|{x/oj,y/John}|
|
|
|
+|knows(John,x)|knows(y,Mother(y))|{y/John,x/Mother(John)}|
|
|
|
+|#knows(John,x)|#knows(x,oj)||
|
|
|
+|knows(John,x)|knows(x,y)|{x/John,y/John}|
|
|
|
+|knows(John,x)|knows(y,x)|{y/John}{y/John,x/Jane}|
|
|
|
+
|
|
|
+__Unification__ is about finding the values that make $\alpha$ and $\beta$ the same for a given row.
|
|
|
+
|
|
|
+An example algorithm that does this is comparing character per character the various strings.
|
|
|
+In the $\theta$ column we find the associations resulting from the comparison.
|
|
|
+For the # formulas there is no substitution that unifies the formulas.
|
|
|
+The last formulas represents a genereal cases that admits more substitutions as solutions.
|
|
|
+
|
|
|
+__MGU__ are the substitutions that are more *general*.
|
|
|
+
|
|
|
+If we have a __knowledge base__
|
|
|
+$$KB\iff\alpha$$
|
|
|
+$$KB\iff$$
|
|
|
+
|
|
|
+In the case of FOL if a substitution is possible, then the right $\theta$ value is returned.
|
|
|
+
|
|
|
+- __forward chaining__
|
|
|
+1. $king(John)$
|
|
|
+2. $(\forall y)Greedy(Y)$
|
|
|
+3. $(\forall x)king(x)\capGreedy(x)\rightarrow Evil(x)$
|
|
|
+4. $Evil(John)$
|
|
|
+
|
|
|
+1-2 are called __facts__ while 3-4 are called __rules__
|
|
|
+
|
|
|
+We can only derive new facts, not rules.
|
|
|
+In FOL it is possible to apply the same rule more than one time, while in Propositional Logic it was useless.
|
|
|
+In the case we have nested functions rules, we can apply them infinite times, this leads to *semi-decidability*.
|
|
|
+
|
|
|
+The quantifiers are needed for every variables to have a __Well Formed Formula__
|
|
|
+
|
|
|
+$\not king(Jane)$ this is not a definite clause and it is not WFF
|
|
|
+$king(John)\cup Greedy(John$ is also not a definite clause because it is not a conjunction of definite clauses.
|
|
|
+
|
|
|
+The main *inference rule* in FOL is called __Modus Ponens_
|
|
|
+$\quotient{p_1'p_2'...p_n' \; p_1\cap p_2\cap ... \cap p_n \rightarrow q}{q\theta}$
|
|
|
+##### example:
|
|
|
+$\quotient{kong(John)\; Greedy(y) \; king(x)\cap Greedy(x) \rightarrow Evil(x)}{Evil(John)}$
|
|
|
+
|
|
|
+#### Exercize
|
|
|
+Demonstrate that colonel West is guilty
|
|
|
+$\exists x \; Missile(x) \cap Owns (Nono,x)$
|
|
|
+$Missile(M)\cap Owns(Nono,M)$
|
|
|
+
|
|
|
+It is possible to prove that these two formulas are not *logically equivalent* (are not the same thing)
|
|
|
+But they are *inferentially equivalent* because you can infere the same results with each of them.
|
|
|
+
|
|
|
+1. $American(x)\cap Weapon(y) \cap Hostile(z) \cap Sells(x,y,z) \rightarrow Criminal(X)$
|
|
|
+2. $Missile(M)$
|
|
|
+3. $Owns(Nono,M)$
|
|
|
+4. $Missile(x)\cap Owns(Nono,x)\rightarrow Sells(West,x,Nono)$
|
|
|
+5. $American(West)$
|
|
|
+6. $Enemy(Nono,America)$
|
|
|
+7. $Missile(x)\rightarrow Weapon(x)$
|
|
|
+8. $Enemy(x,America)\rightarrow Hostile(x)$
|
|
|
+
|
|
|
+I can change the name of the *x* variable with another one because it is *universally quantified*
|
|
|
+Now we would like to prove the following formula.
|
|
|
+
|
|
|
+$\alpha : Criminal(West)$
|
|
|
+
|
|
|
+If we are using forward chaining, we have to apply the rules, as many times as possible.
|
|
|
+
|
|
|
+9. $Sells(West,M,Nono) \; MP(2,3,4) \; \theta ={x/M}$
|
|
|
+10. $Weapon(M) \; MP(2,7) \; \theta ={x/M}$
|
|
|
+11. $Hostile(Nono) \; MP(6,8) \; \theta ={x/Nono}$
|
|
|
+12. $Criminal(West) \; MP(5,10,11,9,1) \; \theta ={x/West, y/M, z/Nono}$
|
|
|
+
|
|
|
+### Algorithm
|
|
|
+Given the goal $\alpha:Criminal(West)$
|
|
|
+- Checks if the goal is already present in the set of rules
|
|
|
+- Then it applies Modus Ponens in a reverse order:
|
|
|
+ - the leafs of the goal node are all the rules required for the father node, and they are considered goals as well.
|
|
|
+- When all the leafs are satisfied i can say that i have
|
