写在前面
我们讲过了命题逻辑中形式推演的两个系统，一个系统由11条规则构成，另外一个系统只有一个规则，这次我们讲一个和归结原理差不多的要给系统霍尔子句和受限制的子句。归结原理实际上是一个搜索的问题，时间复杂度非常高，我们现在引入一个新的概念霍尔子句，是命题逻辑中一个子集，也就是说，对这个KB中每一个具体的sentence他的形式有一个限制。在这些sentence有限制的情况下，我们可以用一套新的规则来推演。在这种有限制的情况下，我们的形式推演系统会变得更加的高效。
限制的概念
我们默认用大写字母表示的都是正文字，加上否之后为负文字
受限制子句definite clauses（还是很多项的析取）：我们这些文字中，有且仅有一个是正文字，其他的都是负的（=1）
霍尔子句horn clauses：最多只有一个为正的子句，正文字。（小于等于1）
Modus Ponens肯定式推理
我们给出一个KB ，我们要根据这个KB推出一个a，只不过在这个时候，我们的KB中每一个sentence都是霍尔子句，a也是霍尔子句，KB是这些霍尔子句的集合。这个时候，我们也有一个规则是Modus Ponens(肯定式推理)。
和归结原理差不多，中间一个横线，上面是前腱，前腱中每一个sentence都是一个霍尔子句，一共有N+1个霍尔子句。右侧是b，我们可以推出来下面的b。
前向推理
为什么有了限制之后，就变得高效了呢？其实很简单，我们要想得到b，就先得到a1到an
前项推理：
检查一下都是霍尔子句
然后KB写成右侧图，每一个node都是一个原子命题，AB假设都有了，我们要推出Q出来，怎么办呢？
我们每一个implication，有多少个原子命题，我们就扫多少轮。
前向推理的可靠性和完备性、
可靠性：跟刚才那个归结原理的时候一样，还是要去证明，N+1项合取之后可以蕴含b
完备性：
后向推理
另外一个算法后向推理：从结论出发推理条件。在计算机实现的时候，用的迭代的思想做的
有一个结论Q，要使得Q成立，要使得p成立……………..
前向推理 VS 后向推理
前向：从条件出发推结论
后向：从结论出发，一般更加高效，因为前项有可能会推出来一些冗余信息，和结论并没有什么关系。
总结
这个时候，我们命题逻辑就讲完了，三套推演规则：一个有11条规则组成。一个是只有一个归结原理。还有一个是KB中句子有了限制。限制为都是霍尔子句，有一个mp规则。每一套归结都是sound也是comple的，所以说命题逻辑是一种declarative声明式的。这种东西首先是可以通过合取析取等方式连接起来。而且我们这种命题逻辑是context-independent（跟上下文无关），所以命题逻辑表达能力有限的
命题逻辑表达能力有限的：比如wupoos中，在深渊旁边有微风，我们在用命题逻辑写这条规则的时候，每一个格子分开写。接下来我们定义一个一阶谓词逻辑，在一阶谓词逻辑中一条规则就可以表述这个东西。
显然在一阶谓词逻辑要重定义我们的language，我们要引入更多的符号，在新的语言下面，我们可以定义形式推演规则，同样在一阶谓词逻辑也有归结原理，也有霍尔子句，也有mp规则。
家庭作业
