AI 一阶逻辑推理
一阶逻辑推理用于从现有句子中推断出新的事实或句子。在理解FOL推理规则之前，让我们了解FOL中使用的一些基本术语。
替换:
替换是对术语和公式执行的基本操作。它以一阶逻辑出现在所有推理系统中。在FOL中存在量词的情况下，替换过程很复杂。如果我们写 F [a/x] ，那么它是指用常量" a "代替变量" x "。
注意: 一阶逻辑能够表达有关宇宙中某些或所有物体的事实。
相等性:
一阶逻辑不仅使用谓词和术语来构成原子句子，而且还使用另一种方式，即FOL中的平等。为此，我们可以使用等号来指定这两个术语指的是同一对象。
示例: 兄弟(John)=史密斯。
与上面的示例一样，兄弟(John)引用的对象与 Smith 所引用的对象相似。等号也可以与否定符一起使用，以表示两个术语不是同一对象。
示例: ￢(x = y)，它等效于x≠y。
量词的FOL推理规则:
作为命题逻辑，我们在一阶逻辑中也有推理规则，因此以下是FOL中的一些基本推理规则:
通用概括
通用实例
现有实例
现有介绍
1、通用概括:
通用概括是一条有效的推理规则，该规则指出，如果前提P(c)对于话语范围中的任意元素c为真，那么我们可以得出结论∀x P(x)。
它可以表示为: 
。
如果我们想证明每个元素都具有相似的属性，则可以使用此规则。
在此规则中，x不得显示为自由变量。
示例: 让我们代表P(c): " 一个字节包含8位"，因此对于∀x P(x) " 所有字节都包含8位。"，这也是正确的。
2、通用实例化:
通用实例化也称为通用消除或UI是有效的推理规则。可以多次应用它以添加新句子。
新的KB在逻辑上等同于先前的KB。
根据用户界面，我们可以推断出用基本词代替变量所获得的任何句子。
UI规则规定，我们可以通过用∀x P(x)代替语篇宇宙中的任何对象来代替基本术语c(域x中的常数)来推断任何句子P(c)。
它可以表示为: 
。
示例: 1、
如果"每个人都喜欢冰淇淋" =>∀xP(x)，那么我们可以推断
"约翰喜欢冰淇淋" => P(c)
示例: 2、
让我们举一个著名的例子
"所有贪婪的国王都是邪恶的。"因此，让我们的知识库以FOL的形式包含以下详细信息:
∀xking(x)∧greedy(x)→Evil(x)，
因此，根据这些信息，我们可以使用通用实例化推断以下任何语句:
国王(John)∧贪婪(John)→邪恶(John)，
国王(理查德)∧贪婪(理查德)→邪恶(理查德)，
国王(父亲(约翰))∧贪婪(父亲(约翰))→邪恶(父亲(约翰))，
3、存在实例化:
存在实例化也称为存在消除，它是一阶逻辑中的有效推理规则。
只能替换一次存在句。
新KB在逻辑上不等同于旧KB，但如果旧KB可以满足，它将可以满足。
该规则指出，对于新的常数符号c，可以从以∃xP(x)形式给出的公式中推断P(c)。
此规则的限制在于，规则中使用的c必须是P(c)为真的新术语。
它可以表示为: 
示例:
从给定的句子中: ∃xCrown(x)∧OnHead(x，John)，
因此我们可以推断: Crown(K)∧OnHead(K，John)，只要K不出现在知识库中即可。
上面使用的K是一个常数符号，称为 Skolem常数。
现有实例是 Skolemization过程的特例。
4、现有介绍
存在性介绍也称为存在性概括，它是一阶逻辑中的有效推理规则。
该规则指出，如果话语宇宙中存在某些具有属性P的元素c，那么我们可以推断出宇宙中存在某些具有属性P的元素。
它可以表示为: 
示例:
" Priyanka的英语成绩很好。"
"因此，某人的英语成绩很好。"
通用模态规则:
对于FOL中的推理过程，我们有一个推理规则，称为通用模态规则。它是Modus ponens的提升版本。
广义模态可概括为: " P表示Q，并且P被断言为真，因此Q必须为真"。
根据Modus Ponens，对于原子词 pi，pi'，q 。如果存在替换θ使得SUBST (θ，pi'，)= SUBST(θ，pi)，则可以表示为:
示例:
我们将使用此规则，因为国王是邪恶的，因此我们将找到一些x，例如x是国王，x是贪婪的，因此我们可以推断出x是邪恶的。
Here let say, p1' is king(John) p1 is king(x)
p2' is Greedy(y) p2 is Greedy(x)
θ is {x/John, y/John} q is evil(x)
SUBST(θ,q).
