37 lines
1.3 KiB
Markdown
37 lines
1.3 KiB
Markdown
|
|
# 简答题
|
|
<ol>
|
|
<li>What is the definition of validity for a propositional logic formula?</li>
|
|
<li>Please explain how to determine whether a given propositional logic formula with CNF is valid.</li>
|
|
<li>Please illustrate the different treatment for free and bound variables in the semantical evaluation of a predicate logic formula.</li>
|
|
<li>Please state the key idea of program verification using model checking techniques.</li>
|
|
</ol>
|
|
|
|
# 计算题
|
|
<ol>
|
|
<li> Convert the following formula into CNF and give its parse tree: $(p \vee q \rightarrow r ) \rightarrow r \vee s$ </li>
|
|
<li> Translate the following statements into predicate logic formula: </li>
|
|
<li> model checking</li>
|
|
</ol>
|
|
|
|
# 证明题
|
|
<ol>
|
|
<li> Prove the following statement: $(p \wedge q) \rightarrow r \vdash (p \rightarrow r) \vee (q \rightarrow r)$</li>
|
|
<li> 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)$</li>
|
|
<li> Prove the total correctness of the following hoare triplet: $\{ x \geq 0 \wedge y > 0 \} Div \{ y=d*x+r \wedge r < y \}$</li>
|
|
|
|
```cpp
|
|
Div:
|
|
{pre-condition}
|
|
r = y;
|
|
d = 0;
|
|
while(r >= y){
|
|
r = r - y;
|
|
d = d + 1;
|
|
}
|
|
{post-condition}
|
|
```
|
|
</ol>
|
|
|