1.写在前面

propositionalize虽然可以做到我们想做到的事，但是它有点没效率。怎么样做更有效率点方法呢？我们来首先来介绍一个，我们叫Generalized Modus Ponens

2.Generalized Modus Ponens

Generalized Modus Ponens，它其实就是Modus Ponens，就是还记得吗，Modus Ponens就是说，你如果知道一个前提，就可以imply这个结论（A=>B），如果我知道前提，那得到的结果就是结论。这是，这个叫做Modus Ponens，那generalized Modus Ponens就是说，我知道这个前提，可是这个前提跟A不太一样，它长的有点像，又有点不像，就是一个A‘，它长的很像A，但是不太一样，但是我还是某种程度上可以的到这个结论，那只要我能找到对的替换，正确的替换，使得A跟A‘一样，那我就可以得到B的结论。

其实这边讲的就是说，如果我知道这些前提嘛，这个P1到Pn，这是我的前提，然后我要导到Q的结论，那我知道这些前提呢，可是我知道的不是exactly p1，我知道的是p1‘，它们长的很像，但是不太一样，然后p2也是跟p2‘一样，有点像，有点不一样，那如果您能找到一个substitution(替代)，也就是说你把p1‘和p1两个，你都用一种substitution Theta，这个substitution带进去，这个Theta可以是任意东西，比如说我们常写的就是，你把x换成John，假设这个样子substitution，会使得左右两边看起来一样。如果对每一个Pi，每一个前提都成立的话，那结果你就会可以得到Q，那当然你也不是直接拿到Q啦，这个Q你也要用同样的Theta去替换，ok。

其实我们刚刚例子，就是我们知道P1,P2,Q,还有和P1,P2相像的两个。ok，那我们就，如果我们能找到一个substitution使得这两个长的一样的话，那Q就可以得到，那我们对应这一个这个KB，你可以看到，如果我刚刚写的p1‘这一个King(John)，那p1是这个King(x)，那你要找到substitution,就是x换成John就好了，对不对，你把x替换成John，那左右两边就长得一模一样，那同样，这边是p2，好，那你只要把x换成y，就长的一模一样，我们刚刚说了，x是John，那你要再把x换成y，所以基本上你就知道，x换成John，而且y换成John，这是你的结论。好，那这样如果你用这个substitution的话，你就会发现，这个左右两式是一模一样的，这样的话，我们就得到这个结论q is Evil(x)，结论不是直接得到的，你要把这个substitutionapply过来，也就是说把里面的x换成John，然后就可以搞定，好，那这样的话就结束。

Modus Ponens apply在KB，基本上指的是definite clause，我们之前有讲过，就是基本上你用CNF的讲法，也就是说，一堆东西的 or  ，那这里面只有一个是正的，其他都是负的，另外一种讲法，就是像我们现在写的，就是这边就是全部都是正的，imply一个正的，好，这样也是一个，也是definite clause。好，那只要是definite clause的话，你可以用generalized Modus Ponens去做。