SharedCourses/计算机逻辑基础/2024秋期末考试（部分）题目.md

简答题

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