From e5dacd67f0e36b9b7b44808869a4d677185d04ec Mon Sep 17 00:00:00 2001 From: Takuyama Date: Thu, 23 Jan 2025 00:10:43 +0800 Subject: [PATCH] =?UTF-8?q?Update=20and=20rename=2024FallFinalExamExcerpt.?= =?UTF-8?q?md=20to=202024=E7=A7=8B=E6=9C=9F=E6=9C=AB=E8=80=83=E8=AF=95?= =?UTF-8?q?=EF=BC=88=E9=83=A8=E5=88=86=EF=BC=89=E9=A2=98=E7=9B=AE.md?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 计算机逻辑基础/2024秋期末考试（部分）题目.md | 36 ++++++++++++++++++++ 计算机逻辑基础/24FallFinalExamExcerpt.md | 9 ----- 2 files changed, 36 insertions(+), 9 deletions(-) create mode 100644 计算机逻辑基础/2024秋期末考试（部分）题目.md delete mode 100644 计算机逻辑基础/24FallFinalExamExcerpt.md 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