diff --git a/计算机逻辑基础/2024秋期末考试（部分）题目.md b/计算机逻辑基础/2024秋期末考试（部分）题目.md new file mode 100644 index 0000000..ee0f12b --- /dev/null +++ b/计算机逻辑基础/2024秋期末考试（部分）题目.md @@ -0,0 +1,36 @@ + +# 简答题 +
    +
  1. What is the definition of validity for a propositional logic formula?
    2. +
  2. Please explain how to determine whether a given propositional logic formula with CNF is valid.
    3. +
  3. Please illustrate the different treatment for free and bound variables in the semantical evaluation of a predicate logic formula.
    4. +
  4. Please state the key idea of program verification using model checking techniques.
    5. +
+ +# 计算题 +
    +
  1. Convert the following formula into CNF and give its parse tree: $(p \vee q \rightarrow r ) \rightarrow r \vee s$
    2. +
  2. Translate the following statements into predicate logic formula:
    3. +
  3. model checking
    4. +
+ +# 证明题 +
    +
  1. Prove the following statement: $(p \wedge q) \rightarrow r \vdash (p \rightarrow r) \vee (q \rightarrow r)$
    2. +
  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. +
  3. Prove the total correctness of the following hoare triplet: $\{ x \geq 0 \wedge y > 0 \} Div \{ y=d*x+r \wedge r < y \}$
    4. + + ```cpp + Div: + {pre-condition} + r = y; + d = 0; + while(r >= y){ + r = r - y; + d = d + 1; + } + {post-condition} + ``` +
+ diff --git a/计算机逻辑基础/24FallFinalExamExcerpt.md b/计算机逻辑基础/24FallFinalExamExcerpt.md deleted file mode 100644 index c80d1a3..0000000 --- a/计算机逻辑基础/24FallFinalExamExcerpt.md +++ /dev/null @@ -1,9 +0,0 @@ -What is the definition of validity for a propositional logic formula? -PLz explain how to determine whether a given propositional logic formula with CNF is valid. - -Please illustrate the different treatment for free and bound variables in the semantical evaluation of a predicate logic formula. - -Please state the key idea of program verification using model checking techniques. - -Prove the following sequent doesn't hold using semantical evaluation: -∀x∃y P(x,y) |- ∃y∀x P(x,y) \ No newline at end of file