{"id":2292,"date":"2022-04-16T19:10:54","date_gmt":"2022-04-16T19:10:54","guid":{"rendered":"https:\/\/mdr.foobrdigital.com\/?p=2292"},"modified":"2022-04-16T19:10:54","modified_gmt":"2022-04-16T19:10:54","slug":"unification-in-fol","status":"publish","type":"post","link":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/2022\/04\/16\/unification-in-fol\/","title":{"rendered":"Unification in FOL"},"content":{"rendered":"\n<h1 class=\"wp-block-heading\">What is Unification?<\/h1>\n\n\n\n<ul><li>Unification is a process of making two different logical atomic expressions identical by finding a substitution. Unification depends on the substitution process.<\/li><li>It takes two literals as input and makes them identical using substitution.<\/li><li>Let \u03a8<sub>1<\/sub>&nbsp;and \u03a8<sub>2<\/sub>&nbsp;be two atomic sentences and ? be a unifier such that,&nbsp;<strong>\u03a8<sub>1<\/sub>? = \u03a8<sub>2<\/sub>?<\/strong>, then it can be expressed as&nbsp;<strong>UNIFY(\u03a8<sub>1<\/sub>, \u03a8<sub>2<\/sub>)<\/strong>.<\/li><li><strong>Example: Find the MGU for Unify{King(x), King(John)}<\/strong><\/li><\/ul>\n\n\n\n<p>Let \u03a8<sub>1<\/sub>&nbsp;= King(x), \u03a8<sub>2<\/sub>&nbsp;= King(John),<\/p>\n\n\n\n<p><strong>Substitution \u03b8 = {John\/x}<\/strong>&nbsp;is a unifier for these atoms and applying this substitution, and both expressions will be identical.<\/p>\n\n\n\n<ul><li>The UNIFY algorithm is used for unification, which takes two atomic sentences and returns a unifier for those sentences (If any exist).<\/li><li>Unification is a key component of all first-order inference algorithms.<\/li><li>It returns fail if the expressions do not match with each other.<\/li><li>The substitution variables are called Most General Unifier or MGU.<\/li><\/ul>\n\n\n\n<p><strong>E.g.<\/strong>&nbsp;Let&#8217;s say there are two different expressions,&nbsp;<strong>P(x, y), and P(a, f(z))<\/strong>.<\/p>\n\n\n\n<p>In this example, we need to make both above statements identical to each other. For this, we will perform the substitution.<\/p>\n\n\n\n<p>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; P(x, y)&#8230;&#8230;&#8230; (i)<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; P(a, f(z))&#8230;&#8230;&#8230; (ii)<\/p>\n\n\n\n<ul><li>Substitute x with a, and y with f(z) in the first expression, and it will be represented as&nbsp;<strong>a\/x<\/strong>&nbsp;and f(z)\/y.<\/li><li>With both the substitutions, the first expression will be identical to the second expression and the substitution set will be:&nbsp;<strong>[a\/x, f(z)\/y]<\/strong>.<\/li><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Conditions for Unification:<\/h2>\n\n\n\n<p><strong>Following are some basic conditions for unification:<\/strong><\/p>\n\n\n\n<ul><li>Predicate symbol must be same, atoms or expression with different predicate symbol can never be unified.<\/li><li>Number of Arguments in both expressions must be identical.<\/li><li>Unification will fail if there are two similar variables present in the same expression.<\/li><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Unification Algorithm:<\/h2>\n\n\n\n<p><strong>Algorithm: Unify(\u03a8<sub>1<\/sub>, \u03a8<sub>2<\/sub>)<\/strong><\/p>\n\n\n\n<pre class=\"wp-block-preformatted\">Step. 1: If \u03a8<sub>1<\/sub> or \u03a8<sub>2<\/sub> is a variable or constant, then:\n\ta) If \u03a8<sub>1<\/sub> or \u03a8<sub>2<\/sub> are identical, then return NIL. \n\tb) Else if \u03a8<sub>1<\/sub>is a variable, \n\t\ta. then if \u03a8<sub>1<\/sub> occurs in \u03a8<sub>2<\/sub>, then return FAILURE\n\t\tb. Else return { (\u03a8<sub>2<\/sub>\/ \u03a8<sub>1<\/sub>)}.\n\tc) Else if \u03a8<sub>2<\/sub> is a variable, \n\t\ta. If \u03a8<sub>2<\/sub> occurs in \u03a8<sub>1<\/sub> then return FAILURE,\n\t\tb. Else return {( \u03a8<sub>1<\/sub>\/ \u03a8<sub>2<\/sub>)}. \n\td) Else return FAILURE. \nStep.2: If the initial Predicate symbol in \u03a8<sub>1<\/sub> and \u03a8<sub>2<\/sub> are not same, then return FAILURE.\nStep. 3: IF \u03a8<sub>1<\/sub> and \u03a8<sub>2<\/sub> have a different number of arguments, then return FAILURE.\nStep. 4: Set Substitution set(SUBST) to NIL. \nStep. 5: For i=1 to the number of elements in \u03a8<sub>1<\/sub>. \n\ta) Call Unify function with the ith element of \u03a8<sub>1<\/sub> and ith element of \u03a8<sub>2<\/sub>, and put the result into S.\n\tb) If S = failure then returns Failure\n\tc) If S \u2260 NIL then do,\n\t\ta. Apply S to the remainder of both L1 and L2.\n\t\tb. SUBST= APPEND(S, SUBST). \nStep.6: Return SUBST. \n<\/pre>\n\n\n\n<h2 class=\"wp-block-heading\">Implementation of the Algorithm<\/h2>\n\n\n\n<p><strong>Step.1:<\/strong>&nbsp;Initialize the substitution set to be empty.<\/p>\n\n\n\n<p><strong>Step.2:<\/strong>&nbsp;Recursively unify atomic sentences:<\/p>\n\n\n\n<ol><li>Check for Identical expression match.<\/li><li>If one expression is a variable v<sub>i<\/sub>, and the other is a term t<sub>i<\/sub>&nbsp;which does not contain variable v<sub>i<\/sub>, then:<ol><li>Substitute t<sub>i<\/sub>&nbsp;\/ v<sub>i<\/sub>&nbsp;in the existing substitutions<\/li><li>Add t<sub>i<\/sub>&nbsp;\/v<sub>i<\/sub>&nbsp;to the substitution setlist.<\/li><li>If both the expressions are functions, then function name must be similar, and the number of arguments must be the same in both the expression.<\/li><\/ol><\/li><\/ol>\n\n\n\n<p><strong>For each pair of the following atomic sentences find the most general unifier (If exist).<\/strong><\/p>\n\n\n\n<p><strong>1. Find the MGU of {p(f(a), g(Y)) and p(X, X)}<\/strong><\/p>\n\n\n\n<p>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; Sol: S<sub>0<\/sub>&nbsp;=&gt; Here, \u03a8<sub>1<\/sub>&nbsp;= p(f(a), g(Y)), and \u03a8<sub>2<\/sub>&nbsp;= p(X, X)<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; SUBST \u03b8= {f(a) \/ X}<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; S1 =&gt; \u03a8<sub>1<\/sub>&nbsp;= p(f(a), g(Y)), and \u03a8<sub>2<\/sub>&nbsp;= p(f(a), f(a))<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; SUBST \u03b8= {f(a) \/ g(y)},&nbsp;<strong>Unification failed<\/strong>.<\/p>\n\n\n\n<p>Unification is not possible for these expressions.<\/p>\n\n\n\n<p><strong>2. Find the MGU of {p(b, X, f(g(Z))) and p(Z, f(Y), f(Y))}<\/strong><\/p>\n\n\n\n<p>Here, \u03a8<sub>1<\/sub>&nbsp;= p(b, X, f(g(Z))) , and \u03a8<sub>2<\/sub>&nbsp;= p(Z, f(Y), f(Y))<br>S<sub>0<\/sub>&nbsp;=&gt; { p(b, X, f(g(Z))); p(Z, f(Y), f(Y))}<br>SUBST \u03b8={b\/Z}<\/p>\n\n\n\n<p>S<sub>1<\/sub>&nbsp;=&gt; { p(b, X, f(g(b))); p(b, f(Y), f(Y))}<br>SUBST \u03b8={f(Y) \/X}<\/p>\n\n\n\n<p>S<sub>2<\/sub>&nbsp;=&gt; { p(b, f(Y), f(g(b))); p(b, f(Y), f(Y))}<br>SUBST \u03b8= {g(b) \/Y}<\/p>\n\n\n\n<p>S<sub>2<\/sub>&nbsp;=&gt; { p(b, f(g(b)), f(g(b)); p(b, f(g(b)), f(g(b))}&nbsp;<strong>Unified Successfully.<br>And Unifier = { b\/Z, f(Y) \/X , g(b) \/Y}<\/strong>.<\/p>\n\n\n\n<p><strong>3. Find the MGU of {p (X, X), and p (Z, f(Z))}<\/strong><\/p>\n\n\n\n<p>Here, \u03a8<sub>1<\/sub>&nbsp;= {p (X, X), and \u03a8<sub>2<\/sub>&nbsp;= p (Z, f(Z))<br>S<sub>0<\/sub>&nbsp;=&gt; {p (X, X), p (Z, f(Z))}<br>SUBST \u03b8= {X\/Z}<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; S1 =&gt; {p (Z, Z), p (Z, f(Z))}<br>SUBST \u03b8= {f(Z) \/ Z},&nbsp;<strong>Unification Failed<\/strong>.<\/p>\n\n\n\n<p><strong>Hence, unification is not possible for these expressions.<\/strong><\/p>\n\n\n\n<p><strong>4. Find the MGU of UNIFY(prime (11), prime(y))<\/strong><\/p>\n\n\n\n<p>Here, \u03a8<sub>1<\/sub>&nbsp;= {prime(11) , and \u03a8<sub>2<\/sub>&nbsp;= prime(y)}<br>S<sub>0<\/sub>&nbsp;=&gt; {prime(11) , prime(y)}<br>SUBST \u03b8= {11\/y}<\/p>\n\n\n\n<p>S<sub>1<\/sub>&nbsp;=&gt; {prime(11) , prime(11)} ,&nbsp;<strong>Successfully unified.<\/strong><br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp;<strong>Unifier: {11\/y}.<\/strong><\/p>\n\n\n\n<p><strong>5. Find the MGU of Q(a, g(x, a), f(y)), Q(a, g(f(b), a), x)}<\/strong><\/p>\n\n\n\n<p>Here, \u03a8<sub>1<\/sub>&nbsp;= Q(a, g(x, a), f(y)), and \u03a8<sub>2<\/sub>&nbsp;= Q(a, g(f(b), a), x)<br>S<sub>0<\/sub>&nbsp;=&gt; {Q(a, g(x, a), f(y)); Q(a, g(f(b), a), x)}<br>SUBST \u03b8= {f(b)\/x}<br>S<sub>1<\/sub>&nbsp;=&gt; {Q(a, g(f(b), a), f(y)); Q(a, g(f(b), a), f(b))}<\/p>\n\n\n\n<p>SUBST \u03b8= {b\/y}<br>S<sub>1<\/sub>&nbsp;=&gt; {Q(a, g(f(b), a), f(b)); Q(a, g(f(b), a), f(b))},&nbsp;<strong>Successfully Unified.<\/strong><\/p>\n\n\n\n<p><strong>Unifier: [a\/a, f(b)\/x, b\/y].<\/strong><\/p>\n\n\n\n<p><strong>6. UNIFY(knows(Richard, x), knows(Richard, John))<\/strong><\/p>\n\n\n\n<p>Here, \u03a8<sub>1<\/sub>&nbsp;= knows(Richard, x), and \u03a8<sub>2<\/sub>&nbsp;= knows(Richard, John)<br>S<sub>0<\/sub>&nbsp;=&gt; { knows(Richard, x); knows(Richard, John)}<br>SUBST \u03b8= {John\/x}<br>S<sub>1<\/sub>&nbsp;=&gt; { knows(Richard, John); knows(Richard, John)},&nbsp;<strong>Successfully Unified.<\/strong><br><strong>Unifier: {John\/x}.<\/strong><\/p>\n","protected":false},"excerpt":{"rendered":"<p>What is Unification? Unification is a process of making two different logical atomic expressions identical by finding a substitution. Unification depends on the substitution process. It takes two literals as input and makes them identical using substitution. Let \u03a81&nbsp;and \u03a82&nbsp;be two atomic sentences and ? be a unifier such that,&nbsp;\u03a81? = \u03a82?, then it can [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[885],"tags":[],"_links":{"self":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/posts\/2292"}],"collection":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/comments?post=2292"}],"version-history":[{"count":0,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/posts\/2292\/revisions"}],"wp:attachment":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/media?parent=2292"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/categories?post=2292"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/tags?post=2292"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}