diff --git a/计算机逻辑基础/24FallFinalExamExcerpt.md b/计算机逻辑基础/24FallFinalExamExcerpt.md
new file mode 100644
index 0000000..c80d1a3
--- /dev/null
+++ b/计算机逻辑基础/24FallFinalExamExcerpt.md
@@ -0,0 +1,9 @@
+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
diff --git a/计算机逻辑基础/lecture01.pdf b/计算机逻辑基础/lecture01.pdf
new file mode 100644
index 0000000..dca7366
Binary files /dev/null and b/计算机逻辑基础/lecture01.pdf differ
diff --git a/计算机逻辑基础/lecture02.pdf b/计算机逻辑基础/lecture02.pdf
new file mode 100644
index 0000000..d5f95c1
Binary files /dev/null and b/计算机逻辑基础/lecture02.pdf differ
diff --git a/计算机逻辑基础/lecture03.pdf b/计算机逻辑基础/lecture03.pdf
new file mode 100644
index 0000000..c0f8482
Binary files /dev/null and b/计算机逻辑基础/lecture03.pdf differ
diff --git a/计算机逻辑基础/lecture04.pdf b/计算机逻辑基础/lecture04.pdf
new file mode 100644
index 0000000..64ea478
Binary files /dev/null and b/计算机逻辑基础/lecture04.pdf differ
diff --git a/计算机逻辑基础/lecture05.pdf b/计算机逻辑基础/lecture05.pdf
new file mode 100644
index 0000000..03b50f9
Binary files /dev/null and b/计算机逻辑基础/lecture05.pdf differ
diff --git a/计算机逻辑基础/lecture06.pdf b/计算机逻辑基础/lecture06.pdf
new file mode 100644
index 0000000..d38b090
Binary files /dev/null and b/计算机逻辑基础/lecture06.pdf differ
diff --git a/计算机逻辑基础/lecture07.pdf b/计算机逻辑基础/lecture07.pdf
new file mode 100644
index 0000000..675f6dc
Binary files /dev/null and b/计算机逻辑基础/lecture07.pdf differ