接下来我们看一下forward chaining的一些特性。
第一个它是既sound又complete，那当然是只有在first-order的d- efinite clause， 那first-order
definite clauses它其实当然不是全部的first-order logic，但他是一个子集，
OK,好，那sound的部分我们就基本上证过了，就是generalized Modus Ponens，
我们有GMP可以证明。那它complete的证明我们这边省略。
但是它如果真的要去证明的话同学可以看一下课本的部分，那其实跟我们上一讲在证明 proposition logic里面证明forward
chaining它是证明法很接近， 但是那时候我们有完整的讲清楚，但是这边的话其实一样类似，就是我们一样，利用fixed
point概念来证明，就是 就是你还是想说说当你forward chaining到一步的时候它不会再导出新的结论的时候 把那地方称为fixed
point，然后之后我们要证明说，就是在这个时间点，我看过的结论，所有 能导出来的东西我们全都把它设为true，然后其它设为false，然后这是一个mod-
el,就是这是一个原来你想证的sentence的model， 那这部分其实跟之前的一样，那有些比较detail的部分我们省略不讲的原因
是因为这边因为有新的，有introduce变出的东西iii，那个地方其实我们的证明- 会变得稍微复杂一点。
其实有点类似像，如果是Modus Ponens的证明它上面我们truth table就可以
它的generalized的版本，我们要稍微花费一些唇舌，讲述这些是怎么被扮演进来- 的。好，那差别就在这边，那概念是一样的。
那，我们在First-Order的 define clause的里面有一种比较，
再小一点，范围再小一点的情况，就是如果我们没有某function， 如果我们在整个knowledge base 里面没有function的话，
那这样特别的一个knowledge base我们称为Datalog， 那其实我们刚刚要证明那个
conenel west是criminal那个KB其实本身没有function，大家可以回想一下，
我们在里面没有定义任何function，那在这种情况下，其实 forward
chaining的时间基本上是polynomial time， 也就说你最多跟我们刚刚讲的，之前一样，你最多有k个变数，然后每一个你最多有n个gr-
ound term， 因为你没有function嘛，所以你ground term就这么多，就只能代换这么多次，然后你有p个这样的sentence，那你就是-
最多换这么多次，也就说 forward chaining一定在time 时间内结束，那一般而言会比这个
效率再快一些，一般而言。通常你可能还没到这个时间点你已经想要，已经得到。但你如果不- 设定这个，就是
你并没有一定的query，你没有 事先前提说我一定要问什么问题，你就让forward chaining 一直跑，
把所有可能能导出来的全部导出来的话，那基本上你时间就这么多，那跟你去proposi- tion来
这个KB，然后用proposition的方法来做结果是一样的。因为我们有讲过for- ward chaining就把所有的function
都会拿出来。所以可以正式证出来。好，那 当然它有个问题，就是它，如果你的，原本要证的某个sentence它如果没有
没有被entail，没有被KB entail的话那它可能根本不会turn in了，这是如果有function的情况下。
这个我们刚刚有提过。那这一个我们也讲过，这是不可能避免的事情，因为基本上entai- lment是first-order logic semi-decidable。
好，这是forward chaining的一些特性。那它的efficiency呢，
它效能来说，基本上我们刚刚那个做法还可以再稍微改进一下，因为一般来说
你如果在第k个，在 就你如果没有任何的前提，在前一个iteration知道的情况下，你在第k个gene-
ration你也不可能得到结论。
啊这个想法我们类似在proposition和logic和forward chaining的时候我们是利用
contour来做这件事情，就是你不用重复的去做unifier的动作。
在propositional logic那边的forward chaining我们是用contour，
就你未知的前提我们先定义一个k,然后，你知道一个你就减，知道一个就减， 那现在这边是因为有变数，因为
你知道是一个p1，那你真正match的是p1,那你如果没事的话去unify p1，其实很浪费时间。
那这边要讲的就是说你如果没有它的前提都没有任何的增加的情况下你不要去做额外的uni- fication。
好，那可是matching本身就是我们去
match，说你哪些有，就是unify这件动作，本身其实很麻烦。就是 如果你用Database
indexing的一些技术我们是可以蛮快的时间譬如说你要问 Missile(x)，你可以蛮快的时间内，由它的database里面有Missil-
e(M1)你可以很快的知道，x是M1。
可是这是单一一个，就是你一个predicate的unify的，很快你可以做到，就是
你用hashing的方式去做indexing。但是如果你要去match多个的时候，- 譬如说像我们下面这个式子， 有两个term要去match，
就蛮困难的，就是因为如果你先match这个，因为答案不止， 你如果match
x它有可能M1，有可能M2、M3， 那接下来如果M1的话你去match这个可能会match失败。
可能normal没有M1，但是可能normal有M3，所以你，也就说这个东西是一个- 搜寻的过程，
你不知道哪一个return的值会使得你在下一个的matching会比较快。
好那基本上我们都有提到，基本上如果是连续的这些，然后
你要找到一个有效率的matching，这个东西，这个问题本身就知道它是一个NP-h- ard， 就是你要得到最有效率的一群它不是一个很简单的问题。
好，那，即使even我们知道我们刚刚提的是forward chaining有这些困难，
有些时候在做matching，就是你先unify A，还是先unify B，这件事情弄不好
就可以做的很没效率，但是anyway，它还是 即使如此还是非常常用，forward chaining常常用在deductive的Database里面。
那接下来我们讲一下backward chaining,因为forward chaining我们讲的比较细一点，那backward
chaining其实概念其实很一样， 其实还是一个and or grave search所以我们基本上就在我们刚刚例子看一下它实际上怎么做就好了。
好，因为backward chaining基本上我们就是有目标嘛，就是离一个目标，我们要证明west是设法证-
明west 是criminal， 那接下来你就去Database里面录入那它需要的前提就是这几个。
你有唯一有match的，你去看它的结论， 结论是criminal(x),如果还记得那个knowledge
base的话，就是你 如果你有一个criminal(x)，则下面这四个前提。
前提。那到这个时间也就是x必须要unify的是west。
好， 然后这样的话你就可以，然后我们在backward chaining的时候未来
记忆体的效率，所以我们都是用dfs， definite
search所以你先优先走这一支，走这一支的时候你就看一下，
American这边我知道x要换成west，就把上面的这一个unify必须往下- 派过来，
所以这边的American的x会变成American(west)，然后你要看一下这- 个American(west)
American(west)是不是可以知道的事实。在我们的case是可以知道，Am- erican(west)是已知的事实。
所以我们就不再需要新的unify了，就可以return回去。
好到下一步如果说是DFS接下来我们走这一支，好这一支是weapon(y)， 那weapon(y)的前提就是Missile(y)，好了Missile(y)的时候-
你再去match一下，那Missile(y)我们 在我们knowledgebase里面有一个Missile(M1)，
好那所以我们就知道我们的y是M1。
所以这是我们新加的unify，那这个新加的unify就必须要return回去的时候- ，整体的unify就增加了一个说x是west，y是M1
这件事情。好接下来再走这一支。
好，走到这边的时候其实你sale的时候其实你这边的x y我们刚刚已经都知道了。
在上一张图片中知道到这边，所以要替换x换成west，
y换成M1。好，那接下来z你去看一下你的knowledgebase里面你就可以知道- z必须要换成Normal。
好，这knowledgebase里面有了一个fact，就是west sale，1, 2,
normal， 好，那这时候我们注意在这个时间点可以知道z是normal，然后一样，要把它
加入你整个的unify。那这个前提呢是 M1是Missile，而且 Normal
owns M1，那这两个前提就check下knowledgebase里面， 其实都有，所以这条路走通了。接着再return再走这条路。
那最后一条路是hussel(x)，hussel(z)的前提就是
我们这边z的时候我们已经在上一步已经知道z是normal了，所以这边会换成nor- mal.
好，然后接下来你会，它的前提是enemy， enemy(z)，america，那你知道
z是Normal所以我们要的是enemy，normal，America，好那你ch- eck一下你的knowledgebase有这条路，
所以就走通了。好这边，所以这边额外需要的unify就不需要了。好到这边其实到这边已- 经做完了，那就return回去，
所以这就是整个backward chaining的过程，然后可以得到的unify就是这种东西。
好那backward chaining的特性呢，就是第一个，它是DF SEARCH， 那因为DF
SEARCH的话它space是linear，就是 space是我们在很早到时候就讲过。
但是整个过程，整个search的过程是在and or search，是在and or graph上search，
