逻辑的一般原理
基于知识的Agent通过对知识的内部表示进行操作而推理，其核心部件是知识库KB，知识库作为语句的集合，用知识表示语言表达，用以表示关于世界的某些断言，某些语句直接给定，我们尊称其为公理；
Agent如何维护其知识库？
- Tell：告诉知识库Agent感知的内容；
- Ask：询问知识库应该采取什么行动，这个过程可能包括大量的推理；
- Tell:告诉知识库Agent选择的行动后并执行；
如果Agent感知到的可用信息正确，那么Agent得出的结论也一定是正确的，这就是逻辑推理的本质；
语法
-
命题：具有确切真值的陈述句；
- 原子命题：不能继续分解的命题；
- 常值命题：不是真就是假的命题；
- 变量命题：没有具体内容的原子命题；
- 复合命题：可以继续分解的命题，由简单命题用括号和联结词组成；
- 简单命题是变量命题时，可看作其函数；
- 原子命题：不能继续分解的命题；
-
联结词：五种常用的联结词如下：
- 否定式:非P，
- 合取式：P且Q，
- 析取式：P或Q，
- 蕴含：规则语句，若P则Q,
- 等价：P当且仅当Q，
-
命题公式：我们递归地定义公式WFF
- 命题变元本身就是公式
- 都是公式；
- 仅通过有限步使用上述两规则进行命题的联结得到的才是公式
对于含有个命题变元的公式,记为;
语义
-
模型/解释：可能的模型就是对命题的真值所有可能赋值，用表示；
对公式,指定的一组真值，这组真值称为的解释；
-
语义：每个命题在每个模型内的真值，命题的真值必须通过指定模型确定；
-
真值表：联结词的运算规则，用如下表来概括
-
逻辑推理：用蕴含关系推导出结论；
- 可靠性：只导出蕴含句的推理算法称为可靠的；
- 完备的：若推理算法可以生成任意蕴含句；
-
模型检验：枚举可能的模型检验KB为真时命题为真,即检验
定理证明
- 逻辑等价：命题 在同样的模型集合中为真，记为
- 有效性（永真性）：若命题在任何模型都是真的；
- 可满足性：若命题在某些模型中为真；
- 永假性：若命题在任何模型都是假的；
永真蕴含式
- 化 简 式 ,
- 附加式,
- 析取三段论
- 假言推理
- 拒取式
- 假言三段论
- 二难推理
- 全称固化
- 存在固化
置换和推理
-
谓词：带有参数的命题；
-
谓词公式的解释：设D是谓词公式P的非空个体域，若对P中的常量，函数和谓词按如下规定赋值:
-
为每个个体常量指派D中的一个元素；
-
为每个n元函数指派一个从Dn到D的一个映射，其中
-
为每个n元谓词指派一个从到{0,1}的映射，则称这些指派为P在D上的一个解释
-
-
谓词公式的永真性：如果谓词公式P对非空个体域D上的任一解释都取得真值T，则称P在D上是永真的；如果P在任何非空个体域上都是永真的，则称P是永真。
-
谓词公式的可满足性：对于谓词公式P，如果至少存在D上的一个解释，使公式P在此解释下的真值为T，则称公式P在D上是可满足的。
-
谓词公式的永假性：如果谓词公式P对非空个体域D上的任一解释都取真值F，则称P在D上是永假的；如果P在任何非空个体域上均是永假的，则称P永假。
-
谓词公式的等价性：设P与Q是D上的两个谓词公式，若对D上的任意解释，P与Q都有相同的真值，则称P与Q在D上是等价的。如果D是任意非空个体域，则称P与Q是等价的，记作P⇔Q。
-
-
在不同谓词公式中，往往会出现谓词名相同但其个体不同的情况，此时推理过程是不能直接进行匹配的，需要先进行置换； W (a) 和W(x)→Q(x)
对谓词W (a)与W (x)谓词名相同，但个体不同，不能直接进行推理。
要使用假言推理，首先需要找到项a对变元x的置换，使W (a)与W (x)一致。这种寻找项对变元的置换，使谓词一致的过程叫做合一的过程。
-
置换是形如
的有限集合。其中，是项；是互不相同的变元； 表示用替换 。要求：与 不能相同，不能循环地出现在另一个 中。
通常，置换是用希腊字母等来表示的
-
设是一个置换，是一个谓词公式，把公式中出现的所有 换成，得到一个新的公式，称为在置换下的例示，记作
归结(消解)演绎推理背景
归结演绎推理是一种基于鲁宾逊(Robinson)归结原理的机器推理技术。鲁宾逊归结原理亦称消解原理, 鲁宾逊于1965年在海伯伦(Herbrand)理论的基础上提出一种基于逻辑的"反证法"
在人工智能中, 几乎所有的问题都可转化为一个定理证明问题。定理证明的实质, 就是对 前提P、结论Q, 证明 P→Q 永真。
要证明P→Q永真, 就要证明P→Q在任何一个非空的个体域上都是永真的。这是非常困难, 甚至是不可实现的。
人们发现可采用反证法的思想, 把关于永真性的证明转化为关于不可满足性的证明。
即要证明P→Q永真, 只要能够证明P∧﹁Q是不可满足的就可。
因 ： ﹁ (P→Q) ⇔ ﹁ (﹁ P∨Q) ⇔ P∧﹁ Q
这方面最有成效的工作就是鲁宾逊归结原理。它使定理证明的机械化成为现实。
