#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$。

*结论：* 推理有效。