我们刚讲的要能apply generalize的Modus Ponens里面有个重要步骤其实就是
其实就是把，找一个substitution，使得这个substitute完以后， p1
prime会等于p1，然后对于每一个前提都能找到这样的substitution。
好，找一个substitution使左边等于右边这件事情其实不是一个很trivia- l的work，
那这个概念我们称它为unification。这个unify
概念其实就是我们return一个，我们称它为unifier，其实unifier就是
众多substitution，里面其中一种可以让左边等于右边的，例如，概念上
就是说我扣这个unifier，然后把p,q丢进去，让它return这个值就是sub- stitution，最好是substitution。
那它能得到目的就是你p1用q substitute完以后跟q用theta去substitute完，结果会一模一样。
好我们来看一下譬如说，这是我的一个例子，这是我的p，这是我的q，
这两个式子，那这是我，这边是我可以的可能能拿到的unify，
那譬如说像这边的话像左边等于右边那你可以基本上是一种比对的方式，
然后就是nose，然后John跟John，就知道x等于Jane。
好那所以我们拿到的substitution就是x替换的这个。
好，那有一些你可以同时unify两个变数，两个以上的变数，
像这个例子的话你可以是John是y嘛，那x是Bill这样，所以你就得到这个subs- titution。
好这几个都OK,那我们substitute也可以替换function，像这里这个例- 子的话我们知道John要
替换成y，然后你的x要换成Mother(y)，
那我们又已知，通常我们会进一步做，因为我们已经知道y是
这个y，刚我们在前一步substitution我们知道是John，所以应该可以 直接把，就是x换成Mother
of John， 这个样子。好，那如果我们要，再看最后一个例子。
如果我们要unify这两个式子， 其实你看John要是x，然后
Eliza要是x，那这一般而言我们应该要会fail， 就是你x不可以用John，Eliza，那如果是是的话你得apply了John=El-
iza， 可是在我们的knowledgebase里面并没有给你这样的资讯，就是
John跟Eliza没有特别声明，或是你没有正常的推论，你不应该假设他们俩是同- 一个人。
好，那这样所以这边会fail，好，可是其实 fail刚这个例子fail，并不是一个
就是我们如果直接看式子，应该是得不到正确的结论，因为x既要是John又是Eliza
那你会John是同一个人，可是，如果我们回头思考那个x这个变数是怎么来的的话， 这其实不是一件，就是
应该让它unify出来，为什么呢，因为这边的x其实是
不代表它指的是同一个东西。就是我们刚这个式子的p的x，
好这个变数，因为我们省略了东西，但这东西可能可以是for x的，
可以是存在x，这是变数来源。好那在这种情况下下面我们已知这一个就是从all x跟存在x 这两个x不需要是同一个。
好，也就是说我们在做unification的时候其实前面之前要先做一件事情叫sta- ndardization，
也就是说，像我们刚那个例子，基本上你应该先把p，
这是p，这是q，你应该先把p,q的变数先standardize，
使得它们不一样就不需要，就不需要一样的就不要一样，就像这个x跟这个x是不需要一样的- ，那通常做法是一个流水后变出一下，
这是x1，看到x2，再看到x3等等。如果把这两个变数 定为不一样的，那你unify结果当然可以是x是Eliza，
x17是John。OK。
好，那其实在一些case里面，unifier 会不止一个。好，譬如说我们看一下下面这个例子。
譬如说如果我们要unify这两个， 好，这个是我的p，还有这个是我的q，这个东西，
那这个，你当然可以给出一件事，就是x,y,z它都是John， 这是第二个，unifier，这样的话左边会等于右边，就是John
knows John， 就左右都长得一模一样，但是这不是一个最generalize的unifier，那一般-
来说我们希望unifier 这个function能return，我们指的是most general unifier。
好，我们简称MGU，那在这个例子里面它的MGU就是应该是
我只要y是John，那接下来x是z就可以了。
OK,那剩下的，就是不过多的去绑定这个sentence， 这个sentence也就是在术语来说，
一般而言我们一个sentence里面的只要是变数， 就是事实我们喜欢叫ground
truth，好，这个大家应该听过，所以ground就是一个弟弟， 那在逻辑上我们常常讲说如果是一个变数的话我们就float，
或说lift，就是把一个ground的term把它举起来， 并一个变数叫lifted，这是我们常用的讲法。也就说反正你在一个
unifier我们最好的事情是不要把一个sentence绑的太死， 就不要把它代的，尽量不要去ground它，
除非必要。好那这样的话return回来就是我们most general的unifier。
好，那你要怎么得到most general unifier
我们在这一讲iii的差异就不再继续， 而且用的技巧是跟
我们前几讲讲的search oren其实类似，它是一个树状结构，然后两边就是等于p and
q，两边同时用 树状结构去展开，然后展到直到某一层两边是长一样的， 那我们就把它们match在一起。那这时候就是如果用
的是那种prefer search就是你用尽量不要往下伸，
也就你return的是最短层数的那一个话通常那一个就是most general的unifier。
好，那另外一个我们提到，因为在这个search unifier的过程其实就是 因为在这个search
unifier的过程其实就是一个搜寻的过程， 那在搜寻的过程我们提到，我们这边提到一个名词叫occur
check，那这个occur check做事情其实是说 某个东西，某个term出现多少次，好，
这个地方我们要讲的过于详细，有同学 对这个有兴趣的同学可能要查，要接触一下比较advance的进阶的人工智慧的课程
接着搜寻技巧，但是一般而言譬如说像我们假设说这是p， 好这是q，这两个sentence，基本上
这两个sentence是不存在unifier，也就说 这两个sentence你不管x带什么东西，它都应该左边不会等于右边因为
右边的式子永远多一个s，对不对，但是如果你做 occur check的话，你就可以了解p不能跟q
unify，但是， occur check要做其实不是一件简单的事情，它类似于要做occur check这件事
类似于在搜寻的过程中要去check某两个space是不是repeat， 是不是已经重复了。
那这件事情我们之前在搜寻的时候就讲过，你如果没有足够的记忆体不见得能够做好这件事
而且写起来，就算你有足够的记忆体写起来你的iii的效率会比较慢一点点。
好，所以其实现在大部分我们晚点就会讲到prologue这个system，大部分逻辑- 演绎的system
其实很多时候是略过occur check的，也就说，很多system我们在实际做的时候，
会使得这个p和这个q这样的会使他们unify，会成立。
这当然结果不是正确的，但是为了一些现实的resource的问题我们不得不这样做。
接下来是一样的事情我们就是我们可以定义一个definite clause，就是first-order definite clause，
如果希望我们的inference更有效率一些的话，那也就是definite clause也就是我们之前提的generalize的Modus
Ponens的一个KB， 好，那原则上我们提醒大家就是exactly one positive literal，
你可以有variable，好我们看一下怎么用definite clause和generalize Modus Ponens来 演绎这个问题。
好，这个问题就是这句话蛮长的，大家可以看一下the law says it
is a crime for an American to sell weapons to hostile nations.
the national Nono, Nono是一个假想的一个国家吧， 没有真的这个国家。OK, anyway，country Nono,
an enemy of America, has some missile,有一些飞弹，然后all of its missiles
were sold to it by Colonel West,好就Colonel West上校卖给他的，上校West又是American，
好但是这整段英文跟我们讲的，我们想要用这一段话证明Colonel West是有罪的。
好我们看一下用first-order logic怎么做。好，首先第一件事情当然是我们要把这一句话把它
先把他transfer成first-order logic的sentence。好，那我们看一下基本上像这句话
前面省略的……就是low sense， it is a crime for an American
to sell weapons to hostile nations,好那基本上就是 你对任何一个人，只要是American，好像我前面其实省略的就是for all了。
好，习惯性， 习惯性是这样接下来我们要做的例子是对一个first-order logic
KB 因为如果有existence的时候我们都会把它用 EI搞定，好，那for
all的情况下呢，一样可以用EI全部弄完，不过那样就回到 propositionalize的过程，所以基本上对for
all我们是保留。existence我们就用EI 把变数换成常数，那也就是说现在接下来我们的first-order
logic KB里面所有的变数都是for all， 那既然说所有变数都是for all我们就不再写for
all这个东西，就大家记得一件事，现在只要看到变数， 我们就是for
all的意思。好，对任何一个x，只要是x是American，然后对任何一个y，只要- y是weapon， 然后x是American
sell了weapon to z，而且z是跟美国是敌对的， 则x就criminal。
好，x就是有罪的。好，那就是基本上你可以看一下就差不多是上面这一句英文的翻译。
就写成逻辑式。好。然后我们接下来有一句senten说Nono这个country有一- 些missiles，
那也就说，存在，你直接写的话是这样，存在某一个x，然后nono有x，而且x是mis- sile，
好，那还是注意下，existence我们对应的是and， 好这我们之前前面有提过。好，到这边你是第一次转换，但到这边时候我们就立刻apply
EI， existence iii把x换成某一个东西。那我们现在换的话就譬如说我们用一个流水号我们就换成M1，
把x换成M1，那接下来这个就是真正到我们KB里面的东西。就把它换成Skolen的c- onstant。
好，那接下来是对所有的missile卖给他的都是， nono所有的missile全都是Colonel
West卖给他的，所以基本上只要 对for
all，所有的x，missile，然后nono又拥有这个x， 则就是West卖x给nono的。
OK,然后，我们的，这是我们基本上的knowledge，就是
missile是weapon，是一种武器，所以只要for all x，对任何的x，
只要x是missile，他就是weapon，大家还是可以注意下我们这边用的for all 对应的是imply。
好，这是这个样子过程。好，那接下来就是任何跟美国敌对的
country我们都认为它有敌意hostile的，所以任何x 只要x是跟American是enemy，就imply它是hostile。
然后，West是American，好这就是我们已知的事实。
然后接下来，country nono是 美国的敌人，这个也是已知的事实。好到这边我们就把整个，
我们上面那一段话以及我们所有知道的knowledge换成first-order logic的一个过程，那接下来就上我们
就可以apply forward chaining， 然后用generalized 的Modus Ponens 去做forward chaining。那forward
chaining其实这边大家看到是个pseudo code， 那其实看这个还好啦，你可以看到这边其实就是Modus Ponens过程在这边。
这边其实就是你只要找到一个substitution使得它的前提都可以对上的情况下，- 我就直接得到这个结论。
OK，然后我们就一直试着去做这件事， 然后在过程中我们要会call
到unify去整合那个substitution，好的，只要找得到 substitution我们就可以试试看。
那接下来我们可以看一下这个forward chaining怎么证明，我们刚转换完了以后我们最后目的 是要证明Colonel
West是criminal的嘛，那我们把我们刚才所有的这几个式子，大家可以看到这- 部有8,
这部有8个式子，好那我们把它换成就写在这边，写在我们的knowledge base，好那我们是一样， ，就是在forward
chaining常常会这样说有implication，他们都，这些列的8个全都是w- hole clause，那或者你要讲definite clause也可以，
那前面这边的，一般来说我们就相当于true，imply, owns，nono and
1， 好，那只是通常我们习惯上，就是让他知道这其实还是一个definite clause，
但是习惯上我会把这个就，但我们不会无聊这样写， 就把这个拿掉，那这一类形式我们通常把它称为fact，
那通常你还有，你里面还有implication的，这个东西我们称为，就里面写成im- plication那有时候也把它称为
rules都可以。好，那基本上我们就回到那forward chaining分为已知的事实还有我们的
规则。好那接下来我们要做forward chaining要做的事情就是把所有可能的， 其实就一样，就把所有可能的事实都导出来，那基本上我们会看一下，
譬如说，如果大家还记得，propositional那边的时候 propositional那边的时候我们就是看一个前提有多少没有被满足，
譬如说第一个generation可以看，就是r5一个check，
这边还有没满足的，premise，OK，这边是就这一个，这个，这个，这个，
然后你去看一下然后发现，你可以找得到一些，可是你没法全部同时找到，所以这个我们就等- 到下一个
iteration来做，但现在好像R6还蛮简单的，R6这是一个p1， p2，这是前提，然后下面得到结论就是Q
那我们看一下，我们已知的事实你会发现这个p1‘ 对，然后你看nono
and1，所以这边是p2’， 然后接下来你就找unifier，然后call unifier就会得到这件事，
就是x就是M1，好，x是M1，这个x就一样，可以套到，就是M1，
OK，这边，好，那就是这个部分。
好，那你就会得到一个结论，结论就是把x换成M1。
得到这个结论， 好，那这个结论一旦得到以后，你就把它加入已知的事实。就是把这个加到已知的事实里面。
然后继续，接下来你看啊，R7也很简单，R7这个missile跟这个很像
missile跟这个很像，就直接把他换成M1，好你就得到这个结论，M1是个wea- pon。
好，那类似我们可以做R8，R8这个enemy跟这个enemy很像，你要替换的就是n- ono，
所以你会得到nono是hostile的，ok。
好，那接下来就第二个generation。
第二个generation这个演绎蛮简单的，因为你得到了这三个，就会发现你得到这一个 然后你会发现这个跟这个很像。
然后，你知道这个结论，这个跟这个很像，
然后你还得到这一个，那这个跟这个很像， 好，接下来最后一个，American呢，是这一个。
这个跟这个很像。
好，就去call unifier，看能不能找到合适的substitution，那实际上是可以找到，
你找到的结果就是x换成West，然后y换成M1，D换成normal就可以搞定。那你- 这些前提都知道以后你就把这个substitution一样
套到它的结论，那这个结论也就说把x换成West。
所以就得到了criminal west。
好，我们来看一下图。那其实这是我们刚， 其实有讲完的啦，其实就这只是用图像来表达一下，这是第一个，
这是第一个，一开始我们知道在non-fact，一开始在KB里面，好这是我的第一个i- teration，
第一个iteration，那我们就能做的事情就是我们刚刚讲的就是这一个，
从这边你会得到这是某一个rule得到的，然后接下来这两个rule，你可以得到这- 个结论，
好这一个又能得到这个结论，所以，第一个iteration里面我会得到新的三个
已知的事实，好接下来就是靠这三个已知的事实来配上我knowledge base里面知道
Colonel West是American就会直接得到West是criminal的，好，在这过程中-
我们这画图不是全部的啦， 只是因为forward chaining基本上说可以导出来，那我们这边画的就是我们可以证出
West是criminal的那一个图。
