85 lines
2.3 KiB
Markdown
85 lines
2.3 KiB
Markdown
---
|
|
title: 2024-2025学年上学期期末
|
|
---
|
|
## 2024-2025学年上学期期末(不全)
|
|
|
|
### 简答题
|
|
|
|
1. What is the definition of validity for a propositional logic formula?
|
|
|
|
2. Please explain how to determine whether a given propositional logic formula with CNF is valid.
|
|
|
|
3. Please illustrate the different treatment for free and bound variables in the semantical evaluation of a predicate logic formula.
|
|
|
|
4. Please state the key idea of program verification using model checking techniques.
|
|
|
|
### 计算题
|
|
|
|
1. Convert the following formula into CNF and draw its parse tree: $(p \vee q \rightarrow r ) \rightarrow r \vee s$
|
|
|
|
2. Translate the following statements into predicate logic formula:
|
|
|
|
3. model checking
|
|
|
|
### 证明题
|
|
|
|
1. Prove the following statement: $(p \wedge q) \rightarrow r \vdash (p \rightarrow r) \vee (q \rightarrow r)$
|
|
|
|
2. Prove the following sequent doesn't hold using semantical evaluation:
|
|
$\forall x \exists y P(x,y) \models \exists y \forall x P(x,y)$
|
|
|
|
3. Prove the total correctness of the following hoare triplet: $\\{ 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}
|
|
```
|
|
|
|
## 人工翻译（仅供参考和学习，实际考试以上文为准）
|
|
|
|
### 简答题
|
|
|
|
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}
|
|
```
|