自动推理的逻辑05--谓词演算

自动推理的逻辑05–谓词演算

什么是谓词逻辑？
命题逻辑将命题变量作为原子命题,可以编码/分析一些重要的系统属性（足以表达 NP 完全问题）
但对于许多建模/分析任务来说，它的表现力还不够,更不用说形式化数学了,甚至苏格拉底的三段论也不能形式化！

无法捕获命题的内部结构，例如
所有的孩子都喜欢冰淇淋。
有的学生理解其中的含义。
没有电子带正电荷。
无法表示诸如“对于所有人”/“存在”之类的量化

推理实体的属性及其关系是不可能的，例如
If x ≤ 7 and 9 ≤ y, then x ≤ y.

更精细的逻辑需要
1 .更具表现力的语言/语法
2 .新的推理规则，用于使用这种语言进行推理
3 .除了命题的真值之外，还有更细粒度的语义

语法应该捕获
条款，例如 2 · x + 6
关系/谓词，例如 x ≤ 7
句子中的量化，例如 “所有 x 都是 φ”或“有些 x 是 φ”

语义应该提供匹配语法表达式的对象、函数和关系;
语义应该允许评估条款，例如 2 · 4 + 6 或 9 ≤ 7 在域中，例如N

命题逻辑回顾
命题逻辑是关于布尔语句的建模：ϕ ::= T | ⊥ | p | ¬ϕ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ),
where p is an atomic proposition.
”1 + 1 = 2” (regarded as a statement)
(p → q) → (¬q → ¬p)
it rains ∨ it shines

谓词逻辑（即一阶逻辑）
谓词逻辑可以描述复杂系统的属性
ϕ ::= > | ⊥ | t1 = t2 | R(t1, . . . ,tn) | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ∃xϕ | ∀xϕ
其中 ti 是术语（表示单个对象），R 是对象。
可以建模和推断对象之间的属性和关系。
公式描述数据结构的属性。
公式对应于数据库查询。

谓词逻辑使用示例Examples on the use of predicate logic

符号
我们再次从自然演绎的基本观点开始
我们用句子作为命题的同义词
公式可能是不完整的句子，例如 “x 是偶数。”
公式的真假可能取决于量词的绑定变量或替换表达式，例如 对他们来说是“苏格拉底”或“5”
我们称可以在公式术语中替换变量的表达式

变量、术语和原子公式Variables, terms, and atomic formulae
变量 x 是单个对象的占位符（例如，7，苏格拉底）（参见命题变量 p 是 0 和 1 的占位符）
术语是单个对象的（复杂）指针;例如，x，x + y，(x) 的母亲
原子公式描述术语之间的关系;例如 祖先,母亲,x ≤ y,
复杂公式是通过使用连接词∧、∨、¬和量词;例如, ∃, ∀
解释将为变量、术语构造函数和关系赋予含义（cf. 在命题逻辑中，赋值解释命题变量)

we write
ϕ(x) for formula ϕ that is parametric in variable x
r,s,t . . . for terms
ϕ[t/x] for result of substituting t for x in ϕ
ϕ(t) to indicate that t occurs in ϕ
例子：
将公式 x ≤ 7 中的变量 x 代入第 5 项,产生句子 5 ≤ 7

参数判断
我们需要对谓词逻辑公式进行新的判断
参数判断
J 表示任意 x,是取决于变量 x 的判断
证据是对 x 的参数 J 的推导
因此，对于我们可以替代 x 的任何项，它都是一致的对于所有可能的情况

参数判断的证据
φ(x) 对于任意 x是 ϕ(x) 的证明模板，可以实例化为任何 ϕ(x)[t/x] 的证明术语 t
多个参数必须在参数推导中保持不同
我们写 a, b, c, . . . 区分参数和普通变量

普遍陈述的证明
最常见的数学语句：
每个A都是B
两个奇数之和是偶数。
任何有限语言的补语都是正则语言。

通用量化Universal Quantification
如果 φ 是公式和 x 变量，则 ∀x.φ 是公式
我们经常写∀x. ϕ(x) 表示 ϕ 取决于 x
我们读到∀x. φ 为“每个 x 都满足 φ”或“每个 x 都是一个 φ”
we can write ∀x.(ϕ(x) ->ψ(x) )
for “Every x satisfies ϕ(x) ->ψ(x) or “Every ϕ is a ψ

推理规则Inference Rules
普遍量化的推理规则是

	--a
	.
	.
	.
	ϕ[a/x]
---------------∀I
    ∀x. ϕ
1
2
3
4
5
6
7

	∀x. ϕ
-----------∀E
	ϕ[t/x]
1
2
3

其中 t 是术语和a是新参数
∀x . φ 是参数判断的证据 φ[a/x]（φ[a/x]的参数证明）
一旦这个证明完成，a 必须在 (∀I) 中被释放

(∀I) 是数学中的标准证明策略
例子：证明 x ∈ X 和 X ⊆ Y 暗示 x ∈ Y 对于所有 x
典型方法：修复任意元素a，为其显示属性

通用量化Universal Quantification
picture

存在量化Existential Quantification
如果 φ 是公式和 x 变量，则 ∃x.φ 是公式
我们读到∃x.φ 为“一些 x 满足 φ”或“存在一个 x 使得 φ”

存在量化的推理规则是

	ϕ[t/x]
----------- ∃I
	∃x. ϕ 
1
2
3

			[ϕ[a/x] ]
			.
			.
			.
∃x. ϕ			ψ
-------------------------∃E
             ψ
1
2
3
4
5
6
7

其中 t 是术语和a是新参数
∃x .φ 是判断 φ[t/x] 的证据
对于一些证人使用∃x.φ 作为假设，我们不需要知道特定的证人

存在量词和析取Existential quantifier and disjunction
存在量词就像一个无限析取
Example
picture

平等
平等很重要
它也有特殊的推理规则

-------------- =I
	t = t
1
2
3

t1 = t2   ϕ[t1/x]
----------------- =E
	ϕ[t2/x]
1
2
3

其中 t, t1, t2 是项
s = t 的证据是 s 等于 t 的证明

示例：相等是对称的：t1 = t2 ` t2 = t1

1. t1 = t2 				hyp
2. t1 = t1 =I  			hyp
3. (x = t1)[t1/x] 		rewriting 1
4. (x = t1)[t2/x] 		=E, 2, 3
5. t2 = t1 				rewriting 4

1
2
3
4
5
6

派生规则
以下派生的相等规则很有帮助

t1 = t2
-------- sym
t2 = t1
1
2
3

t1 = t2   t2 = t3
----------------- trans 
	t1 = t
1
2
3

	t1 = t2
---------------- subst
s[t1/x] = s[t2/x]
1
2
3