exams

CNF/DNF

一般是第一题

技巧

蕴含消除 (Implication Elimination): $A \to B \equiv \neg A \lor B$
内移否定 (De Morgan)： $\neg (A \land B) \equiv \neg A \lor \neg B$ ， $\neg (A \lor B) \equiv \neg A \land \neg B$ 。
消除双重否定： $\neg \neg A \equiv A$

分配律 (Distributivity):
- 生成 CNF (合取范式): 使用 $\lor$ 对 $\land$ 进行分配。 $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$
- 生成 DNF (析取范式): 使用 $\land$ 对 $\lor$ 进行分配。 $A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$
幂等律 (Idempotence)
- $A \land A \equiv A$
- $A \lor A \equiv A$
双向蕴含/等价消除 (Biconditional Elimination): $A \leftrightarrow B \equiv (A \to B) \land (B \to A)$ 或者写成： $A \leftrightarrow B \equiv (\neg A \lor B) \land (\neg B \lor A)$ ,也等价于 $A \leftrightarrow B \equiv (A \land B) \lor (\neg A \land \neg B)$
德摩根定律 (De Morgan's Laws): $\neg (A \land B) \equiv \neg A \lor \neg B$ ， $\neg (A \lor B) \equiv \neg A \land \neg B$
吸收律 (Absorption Laws) - 即你提到的“吞噬”: $A \land (A \lor B) \equiv A$ ， $A \lor (A \land B) \equiv A$ (只要外面有的原子命题出现在里面，且连接词相反，复杂的括号部分就会被“吞噬”)
排中律 (Excluded Middle) 与矛盾律:
- $A \lor \neg A \equiv ⊤$ (True/Valid)
- $A \land \neg A \equiv ⊥$ (False/Contradiction)
常量运算 (Identity & Domination):
- $A \land ⊤ \equiv A$ ,
- $A \land ⊥ \equiv ⊥$
- $A \lor ⊤ \equiv ⊤$ , $A \lor ⊥ \equiv A$
逆否命题 (Contraposition): $A \to B \equiv \neg B \to \neg A$
皮尔士定律 (Peirce's Law): $((A \to B) \to A) \to A$

Formalization

一般是2-4题

命题逻辑 (Propositional Logic) 形式化

描述系统状态（如红绿灯、警报系统）。

当题目问是否 consistent，只要有一组赋值（interpretation）使得所有statement成立即为 consistent。
任意 interpretation 都成立，就是 valid
任意 interpretation 都不成立，就是 inconsistent
有的成立有的不成立就是 invalid
一个statement是invalid，意味着 $T r u e \to F a l s e$

转化关键词

"Unless" (除非) → 通常翻译为 ∨ 或 →。例如 "A unless B" 可以写成 ¬B→A 或 A∨B。
"Only if" (只有当) → A only if B 写作 A→B。
“either or” 写成 $(A \lor B) \land \neg (A \land B)$ , "Exclusive OR"
if A，then B 写成 $A \to B$
A if and only if B 写成 $A ⟺ B$

一阶逻辑 (FOL) 形式化

涉及“所有人”、“存在某个人”、“除了...”的句子

Prolog

一般是第五题（倒数第二题）。

CLP

一般是第六题（最后一题）。

模板

写下 :- use_module(library(clpfd)).
列出变量 List。
用 ins 划定范围。
约束条件, 翻译题目
- 定义Domain
- 定义约束
搜索解:
- labeling([], Vars).
加上注释（%）

语法表

操作	标准 Prolog (不要在建模题用!)	CLP(FD) (考试必须用!)	说明
数值相等	`X is Y + 1`	X #= Y + 1	表示数学等式约束
数值不等	`X =\= Y`	X #= Y	表示 X 不等于 Y
大于/小于	`X > Y`	X #> Y	还有 `#<`, `#>=`, `#=<`
逻辑与	`,` (逗号)	#/	例如 `(X #> 10) #/\ (X #< 20)`
逻辑或	`;` (分号)	#/	例如 `A #= 1 #\/ A #= 2`
逻辑非	`\+`	#	-
互不相同	(手动写递归比较)	all_distinct(List)	极高频考点
绝对值	`abs(X)`	abs(X)	写法一样，但用在约束中

例题

% 0. 引入库
:- use_module(library(clpfd)).

solve(Vars) :-
    % 1. 定义变量 (Variables)
    % 将所有决策变量放入一个列表，方便后续定义域和 labeling
    Vars = [A, B, C, D], 
    
    % 2. 定义域 (Domains)
    % 根据题目设定变量的取值范围
    A in 8 \/ 12 \/ 15 \/ 18 \/ 22,
    B in 0...10,
    Vars ins 10..40, %如果所有变量范围一样就一起写
    
    % 3. 定义约束 (Constraints)
    % 注意：必须使用 # 前缀的运算符 (#=, #>, #\= 等)
    A #>= B,
    C #= A + B,
    all_distinct(Vars),  % 常用全局约束：所有变量值不同
    
    % 4. 搜索解 (Labeling)
    % 这一步触发求解器，将具体数值赋给变量
    labeling([], Vars).

Natural Detuction

自然演绎 (Natural Deduction) 是逻辑学中的一种证明演算系统。不同于基于真值表（Truth Tables）的语义方法（关注什么是“真”的），自然演绎属于证明论（Proof Theory） 的范畴，关注什么是可证明的（syntactic manipulation）,。

它的核心理念是尽可能模仿人类直观的推理方式，“自下而上”地拆解命题，再“自上而下”地通过规则组合出结论,。

1. 核心概念

推导规则 (Inference Rules): 自然演绎不依赖大量的公理，而是通过规则来引入或消除逻辑连接词。每个逻辑连接词（如 $\land, \to, \neg$ ）通常都有一组引入规则 (Introduction Rules, I) 和一组消除规则 (Elimination Rules, E),。
推导树 (Derivation Trees): 证明过程通常表示为树状结构。树叶是假设（Premises/Hypothesis），树根是结论（Conclusion）,。
假设的取消 (Discharge of Assumptions): 在某些规则中（如蕴含引入 $\to I$ 或反证法 RAA），我们可以暂时由一个假设开始推理，得出结论后，将该假设“取消”（通常用方括号 $[ϕ]$ 标记），从而得到不依赖该假设的普遍结论,。

2. 自然演绎例题

以下是根据课程资料和考试题解选取的三个典型例题，展示了不同规则的应用。

例题 1：交换律 (Commutativity of Conjunction)

目标： 证明 $ϕ \land ψ \to ψ \land ϕ$ 来源： 讲义 excerpts,

证明步骤：

假设 $ϕ \land ψ$ 为真（标记为假设 1）。
使用 $\land$ 消除规则 ( $\land E$ )，从假设中拆解出 $ψ$ 。
再次使用 $\land$ 消除规则 ( $\land E$ )，从假设中拆解出 $ϕ$ 。
使用 $\land$ 引入规则 ( $\land I$ )，将 $ψ$ 和 $ϕ$ 组合为 $ψ \land ϕ$ 。
使用 $\to$ 引入规则 ( $\to I$ )，引入蕴含符号，同时取消假设 1。

推导树表示： $$ \frac{ \frac{[\phi \land \psi]^1}{\psi}(\land E) \quad \frac{[\phi \land \psi]^1}{\phi}(\land E) }{ \frac{\psi \land \phi}{\phi \land \psi \to \psi \land \phi}(\to I)_1 } $$

例题 2：矛盾律 (Law of Non-Contradiction)

目标： 证明 $⊢ \neg (F \land \neg F)$ 来源： 2021年6月16日考试题解

证明步骤： 这是一个典型的否定证明。

假设 $F \land \neg F$ 为真（标记为假设 1）。
使用 $\land E$ 得到 $F$ 。
使用 $\land E$ 得到 $\neg F$ （即 $F \to ⊥$ ）。
使用 $\to E$ （或 $\neg E$ ），由 $F$ 和 $\neg F$ 推出矛盾符号 $⊥$ 。
使用 $\neg$ 引入规则（或 $\to I$ ），得出结论 $\neg (F \land \neg F)$ ，并取消假设 1。

推导树表示： $$ \frac{ \frac{[F \land \neg F]^1}{F}(\land E) \quad \frac{[F \land \neg F]^1}{\neg F}(\land E) }{ \frac{\perp}{\neg(F \land \neg F)}(\neg I)_1 } $$

例题 3：连锁推理与归谬法

目标： 证明 $((F \to G) \land (G \to \neg F)) \to \neg F$ 来源： 2021年1月18日考试题解

证明步骤：

假设前提 $(F \to G) \land (G \to \neg F)$ （标记为假设 2）。
为了证明结论 $\neg F$ ，我们先假设 $F$ （标记为假设 1，准备进行反证）。
从假设 2 中拆解出 $F \to G$ 。结合假设 $F$ ，通过 $\to E$ 推出 $G$ 。
从假设 2 中拆解出 $G \to \neg F$ 。结合上一步得到的 $G$ ，通过 $\to E$ 推出 $\neg F$ 。
现在我们要么得到了 $\neg F$ （直接证明），要么如果你视 $\neg F$ 为 $F \to ⊥$ ，则结合 $F$ 得到 $⊥$ 。
此处题解使用了归谬法（RAA）或否定引入：由 $F$ 导出了矛盾（因为同时也导出了 $\neg F$ ），所以 $F$ 不成立，即 $\neg F$ 。
最后通过 $\to I$ 取消假设 2，得出最终蕴含式。

推导树表示： $$ \frac{ [((F \to G) \land (G \to \neg F))]^2 }{ \frac{G \to \neg F}{}(\land E) } \quad \frac{ \frac{[((F \to G) \land (G \to \neg F))]^2}{F \to G}(\land E) \quad [F]^1 }{ G }(\to E) $$ （注：上述两部分结合推出 $\neg F$ ，再与 $[F]^{1}$ 结合推出 $⊥$ ，最后通过规则得到 $\neg F$ 并取消假设 1 和 2，最终形成完整树形结构）。

2025 jan

基于提供的 2023年1月12日 (Exam 23.01.12) 试题内容，以下是前两道题目的详细解答和解题思路。

由于提供的参考答案文件中似乎没有包含这两题的具体步骤（通常考试官方解答有时只给结论），这里我根据逻辑学（自然演绎和语义判定）的标准规则为你重新推导一遍。

Q1. 自然演绎证明 (Natural Deduction)

题目 1.1: 证明 $⊢ (A \to (B \to C)) \to ((A \land B) \to C)$

解题思路： 这是一个标准的蕴含证明。我们需要证明的主连接词是 →，所以策略是：

假设前件 A → (B → C)。
为了证明后件 (A ∧ B) → C，再次假设 A ∧ B。
利用 ∧E (消除合取) 拆解 A ∧ B 得到 A 和 B。
利用 →E (蕴含消除/Modus Ponens) 结合 A 和第一个假设，得到 B → C。
再次利用 →E 结合 B 和 B → C，得到 C。
最后使用 →I (蕴含引入) 两次，取消假设，得到结论。

证明树 (Derivation Tree):

\frac{\frac{[A \to (B \to C)]^{1} \frac{[A \land B]^{2}}{A} (\land E)}{B \to C} (\to E) \frac{[A \land B]^{2}}{B} (\land E)}{\frac{C}{(A \land B) \to C} (\to I)^{2}} (\to I)^{1}

假设 1: $A \to (B \to C)$
假设 2: $A \land B$

推导步骤：

Step A: 从假设 2 ( $A \land B$ ) 使用 $\land E$ 得到 $A$ 。
Step B: 从假设 2 ( $A \land B$ ) 使用 $\land E$ 得到 $B$ 。
Step C: 使用假设 1 和 Step A 的结果 ( $A$ )，通过 $\to E$ 得到 $B \to C$ 。
Step D: 使用 Step C 的结果 ( $B \to C$ ) 和 Step B 的结果 ( $B$ )，通过 $\to E$ 得到 $C$ 。
Step E: 取消假设 2，通过 $\to I$ 得到 $(A \land B) \to C$ 。
Step F: 取消假设 1，通过 $\to I$ 得到最终结论 $(A \to (B \to C)) \to ((A \land B) \to C)$ 。

这个证明的核心在于先把复杂的蕴含式拆解，利用合取拆分出的原子命题进行“喂入”，最后得到结论 $C$ 后再层层打包回去。希望这次的展示更加清晰！

题目 1.2: 证明或找反例 (F → G) → (¬G → F)

解题思路： 我们需要检查这个公式是否恒真（Tautology）。观察后件 ¬G → F。如果 G 是假 (False)，¬G 就是真。此时如果 F 也是假，那么 ¬G → F 就是 True → False，结果为假。再看前件 F → G。如果 F 是假，G 是假，那么 F → G是 False → False，结果为真。 综上： 前件真，后件假，整个蕴含式为假。所以这是一个**非有效（Not Valid）**的公式，不能证明，需要给出反例。

反例 (Counter-example):

令解释 $I$ 为： $F = F a l s e (⊥), G = F a l s e (⊥)$
前件验证： $F \to G \equiv ⊥ \to ⊥ \equiv ⊤$ (True)
后件验证： $\neg G \to F \equiv \neg ⊥ \to ⊥ \equiv ⊤ \to ⊥ \equiv ⊥$ (False)
结论： $⊤ \to ⊥ \equiv ⊥$ (False)。公式不成立。

Q2. 逻辑蕴含判定 (Logical Consequence)

题目要求判断 $ϕ ⊨ ψ$ 是否成立（即 $ψ$ 是否是 $ϕ$ 的逻辑结果）。如果不成立，需给出反例。

题目 2.1:

$ϕ$ : $(A \to B) \land (A \to C)$
$ψ$ : $\neg B \lor \neg C \lor A$

解题思路 (寻找反例法): 我们要找一个解释 $I$ ，使得 $ϕ$ 为真 ( $T r u e$ ) 而 $ψ$ 为假 ( $F a l s e$ )。

让 $ψ$ 为假：
- $\neg B \lor \neg C \lor A$ 为假，意味着所有析取项都必须为假。
- $\neg B$ 是 False $\Rightarrow$ $B = T r u e$
- $\neg C$ 是 False $\Rightarrow$ $C = T r u e$
- $A$ 是 False $\Rightarrow$ $A = F a l s e$
检查在解释 $I : A = F, B = T, C = T$ 下， $ϕ$ 是否为真：
- $A \to B \equiv F \to T \equiv T r u e$
- $A \to C \equiv F \to T \equiv T r u e$
- $ϕ \equiv T r u e \land T r u e \equiv T r u e$ 。
结论： 存在一个解释使得前件真后件假，所以 $ϕ ⊭ ψ$ (Not a logical consequence)。

题目 2.2:

$ϕ$ : $A \lor B \lor \neg C$
$ψ$ : $(A \land B) \to C$

解题思路 (寻找反例法): 试图让 $ϕ$ 为真， $ψ$ 为假。

让 $ψ$ 为假：
- 蕴含式 $(A \land B) \to C$ 只有在“前件真且后件假”时才为假。
- 所以必须满足： $A \land B$ 为真 $\Rightarrow$ $A = T r u e, B = T r u e$ 。
- 同时 $C$ 为假 $\Rightarrow$ $C = F a l s e$ 。
检查在解释 $I : A = T, B = T, C = F$ 下， $ϕ$ 是否为真：
- $ϕ = A \lor B \lor \neg C \equiv T \lor T \lor \neg F \equiv T r u e$ 。
结论： 存在反例 $I : A = T, B = T, C = F$ ，所以 $ϕ ⊭ ψ$ (Not a logical consequence)。

总结

Q1.1: 可通过自然演绎证明。
Q1.2: 不成立，反例为 $F = F, G = F$ 。
Q2.1: 不成立，反例为 $A = F, B = T, C = T$ 。
Q2.2: 不成立，反例为 $A = T, B = T, C = F$ 。