SharedCourses/docs/courses/软件工程学院/计算机逻辑基础/2024Fall_期末_不全.md

title	category	tag	author
2024Fall_期末_不全	软件工程学院 试卷	期末	タクヤマ

简答题

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 \\}

Div:
  {pre-condition}
  r = y;
  d = 0;
  while (r >= y) {
    r = r - y;
    d = d + 1;
  }
  {post-condition}