Update and rename 24FallFinalExamExcerpt.md to 2024秋期末考试（部分）题目.md

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

@@ -0,0 +1,36 @@
+
+# 简答题
+<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>
+

计算机逻辑基础/24FallFinalExamExcerpt.md

@@ -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)