diff --git a/docs/undergraduate/软件工程学院/计算机逻辑基础/2024-2025学年上学期期末.md b/docs/undergraduate/软件工程学院/计算机逻辑基础/2024-2025学年上学期期末.md
index 8aa4712..d6baa89 100644
--- a/docs/undergraduate/软件工程学院/计算机逻辑基础/2024-2025学年上学期期末.md
+++ b/docs/undergraduate/软件工程学院/计算机逻辑基础/2024-2025学年上学期期末.md
@@ -41,3 +41,44 @@ Div:
   }
   {post-condition}
   ```
+
+## 人工翻译（仅供参考和学习，实际考试以上文为准）
+
+### 简答题
+
+1. 命题逻辑公式的有效性的定义是什么?
+
+2. 请解释如何判断一个给定的带有合取范式形式的命题逻辑公式是否是有效的
+
+3. 请描述一下在谓词逻辑公式的语义评估中，如何处理自由变量和约束变量
+
+4. 请阐述使用模型检测技术进行程序验证的核心思想
+
+### 计算题
+
+1. 将下面的公式转换为合取范式，并且画出它的分析树 $(p \vee q \rightarrow r ) \rightarrow r \vee s$
+
+2. 将以下语句翻译为谓词逻辑公式
+
+3. 模型检测
+
+### 证明题
+
+1. 证明以下命题: $(p \wedge q) \rightarrow r \vdash (p \rightarrow r) \vee (q \rightarrow r)$
+
+2. 使用语义评估来证明以下矢列不成立:
+  $\forall x \exists y P(x,y) \models \exists y \forall x P(x,y)$
+  
+3. 证明以下霍尔三元组的完全正确性: $\\{ x \geq 0 \wedge y > 0 \\} Div \\{ y=d*x+r \wedge r < y \\}$
+
+```cpp
+Div:
+  {pre-condition}
+  r = y;
+  d = 0;
+  while (r >= y) {
+    r = r - y;
+    d = d + 1;
+  }
+  {post-condition}
+  ```
diff --git a/docs/undergraduate/软件工程学院/计算理论基础/2024-2025学年下学期期末.md b/docs/undergraduate/软件工程学院/计算理论基础/2024-2025学年下学期期末.md
index 3699693..7f3bbfe 100644
--- a/docs/undergraduate/软件工程学院/计算理论基础/2024-2025学年下学期期末.md
+++ b/docs/undergraduate/软件工程学院/计算理论基础/2024-2025学年下学期期末.md
@@ -13,7 +13,10 @@ title: 2024-2025学年下学期期末
 
 3. A marble is dropped at A and B. Levers x1, x2 and x3 cause the marble to fall either to the left or to the right. Whenever a marble encounters a lever, it causes the lever to reverse after the marble passes, so the next marble will take the opposite branch. The game wins when there is a marble falls through C. The levers are all initialized to the left. Model this toy by a DFA.
 
-    ![marble](./assets/marble.png)
+>这里是人工翻译：
+在 A 点和 B 点分别掉落一个弹珠。控制杆 x1, x2, x3 会使弹珠向左或向右落下。每当弹珠经过任意一个控制杆，总会使控制杆反转，使得下一个弹珠选择另一个岔路。当存在一个弹珠掉落到 C 点使游戏胜利。拉杆初始全部设置为向左。请用 DFA 为这个小玩具建模。
+
+![marble](./assets/marble.png)
 
 4. 证明语言 $L = \{a^nb^nc^md^m (n \geq m \geq 1) \cup a^nb^mc^md^n (n \geq m \geq 1)\}$ 不是 CFL