ch07-ch09 report finished
This commit is contained in:
3255
logic/main.pdf
Normal file
3255
logic/main.pdf
Normal file
File diff suppressed because it is too large
Load Diff
96
logic/main.typ
Normal file
96
logic/main.typ
Normal file
@ -0,0 +1,96 @@
|
||||
#set page(paper: "a4", margin: 2cm)
|
||||
#set text(font: ("Noto Sans CJK SC", "SimSun"), size: 10.5pt)
|
||||
#set heading(numbering: "1.")
|
||||
|
||||
#align(center)[
|
||||
#block(text(weight: "bold", size: 18pt)[人工智能课程ch07-09逻辑作业报告])
|
||||
]
|
||||
|
||||
= 命题逻辑合取范式转换
|
||||
*题目:* 求 $(P and (Q -> R)) -> S$ 的合取范式。
|
||||
|
||||
*解答:*
|
||||
1. 消去蕴含符号:
|
||||
$ not (P and (not Q or R)) or S $
|
||||
2. 应用德·摩根定律:
|
||||
$ (not P or not (not Q or R)) or S $
|
||||
$ (not P or (Q and not R)) or S $
|
||||
3. 应用分配律:
|
||||
$ ((not P or Q) and (not P or not R)) or S $
|
||||
4. 再次应用分配律(将 $S$ 结合进去):
|
||||
$ (not P or Q or S) and (not P or not R or S) $
|
||||
|
||||
*最终结果:* $(not P or Q or S) and (not P or not R or S)$
|
||||
|
||||
|
||||
= 复合语句分析
|
||||
*题目:* 考虑语句 $[((F or D) => P) or (M => P)] => [(F and M) => P]$ (简写变量名)。
|
||||
|
||||
*(a) 通过枚举模型判断有效性:*
|
||||
设 $F, D, M, P$ 为布尔变量。考虑一种情况:使结论 $(F and M) => P$ 为假。
|
||||
只有当 $F=T, M=T, P=F$ 时,结论为假。
|
||||
代入左边:$[((T or D) => F) or (T => F)] equiv [F or F] equiv F$。
|
||||
由于“假 $=>$ 假”为真,该语句在所有使结论为假的解释下依然为真。经穷举,该语句在所有解释下均为真。
|
||||
*结论:* 该语句是 *有效的 (Valid)*。
|
||||
|
||||
*(b) 转换为合取范式 (CNF):*
|
||||
左边 (L):$((F or D) => P) or (M => P)$
|
||||
$ equiv (not(F or D) or P) or (not M or P) $
|
||||
$ equiv (not F and not D) or P or not M or P $
|
||||
$ equiv (not F or not M or P) and (not D or not M or P) $
|
||||
|
||||
右边 (R):$(F and M) => P equiv not F or not M or P$
|
||||
|
||||
全式 $L => R equiv not L or R$:
|
||||
由于 $R$ 已经是 $L$ 的一个合取项,根据 $(A and B) => A$ 永远为真,转换结果支持了有效性结论。
|
||||
|
||||
|
||||
= 一阶逻辑翻译 (基础谓词)
|
||||
*题目要求:使用给定谓词表示语句。*
|
||||
|
||||
1. *有一门课所有老师都教授:*
|
||||
$ exists c ("Course"(c) and forall t ("Teacher"(t) => "Teach"(t, c))) $
|
||||
|
||||
2. *恰有一门课由 "Alice" 教授且被 "Bob" 选修:*
|
||||
$ exists c ("Course"(c) and "Teach"("Alice", c) and "Study"("Bob", c) and forall c' (("Teach"("Alice", c') and "Study"("Bob", c')) => c = c')) $
|
||||
|
||||
3. *所有老师教授的课程都至少有一个学生选修:*
|
||||
$ forall t forall c (("Teacher"(t) and "Teach"(t, c)) => exists s ("Student"(s) and "Study"(s, c))) $
|
||||
|
||||
4. *有一个学生选修了 "Alice" 教授的所有课程:*
|
||||
$ exists s ("Student"(s) and forall c ("Teach"("Alice", c) => "Study"(s, c))) $
|
||||
|
||||
|
||||
= 一阶逻辑翻译 (自定义谓词)
|
||||
*自定义谓词:* $"Fail"(s, c)$ 表示 $s$ 考试缺考;$"Pass"(s, c)$ 表示 $s$ 通过课程 $c$;$"Borrow"(s, b)$ 表示学生 $s$ 借阅书 $b$。
|
||||
|
||||
1. *有老师只教授了一门课程:*
|
||||
$ exists t ("Teacher"(t) and exists c ("Teach"(t, c) and forall c' ("Teach"(t, c') => c' = c))) $
|
||||
|
||||
2. *如果一名学生缺考,他就无法通过该课程:*
|
||||
$ forall s forall c (("Student"(s) and "Course"(c) and "Fail"(s, c)) => not "Pass"(s, c)) $
|
||||
|
||||
3. *没有一本书被两名学生同时借出:*
|
||||
$ not exists b exists s_1 exists s_2 ("Book"(b) and "Student"(s_1) and "Student"(s_2) and s_1 != s_2 and "Borrow"(s_1, b) and "Borrow"(s_2, b)) $
|
||||
|
||||
|
||||
= 推理有效性论证 (归结证明法)
|
||||
*前提:* 所有的智能手机都是电子设备。 $forall x ("Smartphone"(x) => "ElectronicDevice"(x))$
|
||||
*结论:* 任何智能手机的制造商都是电子设备制造商。 $forall x forall y (("Smartphone"(x) and "ManufacturedBy"(x, y)) => exists z ("ElectronicDevice"(z) and "ManufacturedBy"(z, y)))$
|
||||
|
||||
*归结证明步骤:*
|
||||
1. *前提子句化:*
|
||||
$C_1: not "Smartphone"(x) or "ElectronicDevice"(x)$
|
||||
2. *结论否定并子句化:*
|
||||
$not [forall x forall y (("Smartphone"(x) and "ManufacturedBy"(x, y)) => exists z ("ElectronicDevice"(z) and "ManufacturedBy"(z, y)))]$
|
||||
引入常量 $S, M$ (Skolemization):
|
||||
$C_2: "Smartphone"(S)$
|
||||
$C_3: "ManufacturedBy"(S, M)$
|
||||
$C_4: not "ElectronicDevice"(z) or not "ManufacturedBy"(z, M)$
|
||||
3. *推导矛盾:*
|
||||
- 由 $C_1$ 和 $C_2$ (置换 $\{x/S\}$): $"ElectronicDevice"(S) (C_5)$
|
||||
- 由 $C_4$ 和 $C_3$ (无法直接归结,但由于 $S$ 满足 $"ManufacturedBy"(S, M)$):
|
||||
将 $C_4$ 中的 $z$ 置换为 $S$: $not "ElectronicDevice"(S) (C_6)$
|
||||
- $C_5$ 与 $C_6$ 归结产生空子句 $square$。
|
||||
|
||||
*结论:* 推理有效。
|
||||
Reference in New Issue
Block a user