一、写在前面
这个课程已经讲了很多东西了，之前有一个老师，讲了搜索，讲了机器学习，讲了深度学习，讲了对抗学习，讲了CV和常见序列模型，每一节课都挖了一个大坑，需要我慢慢的填补。我太南了。现在是一个计算所老师讲解知识表示，知识推理这部分内容，老师课件设置合理，每节课都可以学到具体的知识点，而非大而空的概念。因此，打算在更新了搜索之后，更新知识这个模块。
参考资料：
用的教材是《人工智能》，*大学于天立公开课
这门课涉及到数理逻辑，参考《数理逻辑》陆钟万，也有参考视频
二、基本概念：
知识推理和表示，需要把知识表示为一个知识库的形式。这个知识库是一个集合，在这个集合中有很多sentence，每一个sen都符合一个形式上的语言，我们有了这个知识库之后，我们希望可以向这个知识库提问问题。
怎么提问问题？我们采用declarative 声明的形式提问题，问了之后，知识库有一个自动的引擎，你可能并不知道这个引擎内部实现，但是知识库可以利用这个引擎可以回答我们的问题。这个引擎是一个通用的引擎，不用关心怎么实现，编程的时候，你就告诉他，构建知识库，同时可以在这个知识库上提问，答案可以自动出来。
举个例子：定理的自动证明，首先在knowledge base中放入基本的定理，公理。另外inference engine可以自动生成其他的性质。或者我们给一个新的新的性质，可以判断是否真假。
老师上课讲的是一种形式上的逻辑，我们用头脑中的逻辑研究形式上的逻辑，这个是一种嵌套关系。形式逻辑是一种形式语言，我们定义一套语言，肯定会定义一套语法，规定什么样的语言是合法的。另外我们还关注sen的语义，看哪个sen是真，哪个是假。
这幅图是这节课的经典：
- 1.逻辑研究的内容是研究形式化定义的sentences之间的关系
- 2.知识库是sen的集合，每一个sen都符合形式逻辑规定的语法，老师每讲一个逻辑就会讲这个逻辑规定的语法，哪一些语言是合法的sen，哪一些不是，有了语言才能形式逻辑
- 3.老师会讲两种逻辑：命题逻辑+一阶谓词逻辑
- 4.每一个逻辑都有两个内容：从语义的角度能够蕴含一些新的知识库（新的知识，是正确的）。还会从语法的角度推演，自动推演出新的知识库（每一个sen都是一堆符号，通过形式上推演，推演出新的sen，这个和语义无关，是从符号上推演出的一种规则）
- 5.对上面总结：每一个逻辑含有两个内容：语义上蕴含+形式上推演
- 6.我们会证明两个性质：可靠性和完备性
- 7.语义上蕴含（逻辑推导）和形式上推演都会得到一个知识库，我们可以将其看做sen的集合
- 8.左侧是语义蕴含，右侧是形式上推演
- 9.如果左侧的集合是右侧的子集，我们说是完备的（没有少推一些东西）
- 10.如果右侧的集合是左侧的子集，我们说是可靠的（推出来是对的）
- 11.如果右侧的集合是左侧集合的子集，我们可以说这一套逻辑是可靠的，意思是，我形式上推演出来的sen在语义上是对的，我每推出一个东西他是对的，所以我们可以认为他是可靠的。
- 12.如果左侧的集合是右侧集合的子集，我们说这一套逻辑是完备的，意思是：任何能够从语义上面推出来的正确的东西，我都可以从形式上的方式推演得到，我们说这一套规则是完备的
- 13.通常来说，定义一套逻辑，我们都要定义它的语义和语法规则（形式的推演规则），这种形式推演规则不是乱定义的，我定义完了之后，我们要进行测试，是否完备和可靠。
- 14.接下来讲命题逻辑和一阶谓词逻辑，都会分别讲他的语义蕴含和语法推演
三、语义entailment
证明一：KB |= a 等价于 M（KB）含于 M（a）
四、命题逻辑
接下来，我们看一下命题逻辑（propositional logic），任何一个逻辑都有自己的语言，我们会看这个逻辑的syntax语法和semantics语义两个部分。
4.1 语法syntax
概念部分：
命题：一个声明sen（太阳从东方升起），有可能是真有可能为假。这个声明与时间无关，不随着时间变化真假，如果该命题真假与时间有关，这不是我们考察的范围。
原子命题：atomic propositions 不可拆分 ，原子命题用大写字母表示，每一个表示原子命题的大写字母都是一个合法的sentence。
文字：literals 表示为原子命题或者原子命题的反
除此之外，在命题逻辑中还定义了其他5个符号，这5个符号是在语言中被允许的符号，negation conjunction disjunction implication biconditional取一个名字，不要去想他的含义。这些都是定义的合法的language
复合命题：complexSentence 是由原子命题和下面五个符号组合而成。
每一个符号，我们都给了对应关系，我们规定了真值表。通过真值表可以推演其他复合命题
这个是真值表，要记住
4.2 inference 逻辑推理
我们给了一个KB知识库之后，这个KB中每一个sen都是命题逻辑中的sen，都是合法的sen，α 现在是另外一个合法的sen，证明KB是否entailment α 成立（蕴含 ），有没有一个自动化的算法来验证这个问题？
这个算法过程叫inference推理
我们任意找到一个model，如果使得KB里面每一个sen成立，那么这个model一定要使得α 为真
假设KB中原子命题有N个，他的model一共有2^n ，每一个model试一下KB，试一下α，如果都是为真，就成立了。
4.3 语义上逻辑等价：logical equivalence
If a entailment b 且 b entailment a 则成为逻辑等价，logically equivalent （三个横）
4.4 区分语义上蕴含entailment和命题运算中的implication
Entailment 是语义上的蕴含 KB entailment a
Implication 是命题之间的运算子，使用真值表刻画其语义 { 右箭头 爆炸 假假、假真、真真为真 ，真假为假 implication}
证明二：KB |= a,当且仅当 KB=>a（右箭头）爆炸 假假、假真、真真为真 ，真假为假 implication
