diff --git a/class_12_04092023/summary.txt b/class_12_04092023/summary.txt
new file mode 100644
index 0000000..dd44d1a
--- /dev/null
+++ b/class_12_04092023/summary.txt
@@ -0,0 +1,10 @@
+Class 12 : Normal Forms 
+-- literals, positive literals, negative literals. 
+-- CNF, DNF  
+-- existence of  equivalent formulae in CNF and DNF for a given formula using truth tables 
+-- time complexity of SAT -- NP complete
+-- quest for some fragment which has polytime complexity for SAT
+-- Horn formulae : CNF with each clause having at most one literal
+-- Algorithm for checking satisfiability of Horn Formulae 
+
+ 
diff --git a/class_13_05092023/summary.txt b/class_13_05092023/summary.txt
new file mode 100644
index 0000000..22438f2
--- /dev/null
+++ b/class_13_05092023/summary.txt
@@ -0,0 +1,18 @@
+Class 13 : Horn Formulae 
+  
+Horn Formulae : CNF with each clause having at most one positive literal. 
+Algorithm for satisfiability-greedy algo
+Termination proof
+Time complexity-polytime
+Correctness.
+Soundness : If alogH says formula \alpha is satisfiable then \alpha is satisfiable.
+Proof idea : algoH gives an assignment, we prove that this satisfies \alpha. 
+ 
+Completeness:  If the given formula \alpha is satisfiable then algoH prints "satisfiable".
+Proof idea: Prove the contrapositive of above statement, using the following claim.
+ 
+Claim : if a proposition is marked true then it remains true in all
+possible satisfying assignments of the given Horn Formulae
+
+-- Horn formulae satisfying algorithm and Prolog. 
+
diff --git a/class_14_07092023/summary.txt b/class_14_07092023/summary.txt
new file mode 100644
index 0000000..94649a0
--- /dev/null
+++ b/class_14_07092023/summary.txt
@@ -0,0 +1,18 @@
+Class 14 : *** Proof system for logic
+ 
+** Desirable properties of a proof system 
+** Proof systems has a set of axioms (AXIOMS) and rules (R). 
+** Set of formulas provable in the system = I(AXIOMS, R). 
+   Alternatively, provable formulas have legal construction sequences over AXIOMS and R. 
+ 
+**  Hilbert's proof system for Propositional Logic:  
+*   Axioms : 
+* 	Ax1 : (\alpha --> (\beta --> \alpha))
+* 	Ax2 : ( (\alpha --> (\beta --> \gamma)) --> ((\alpha --> \beta) --> (\alpha --> \gamma)) )
+* 	Ax3 : ( (\neg \beta --> \neg \alpha) --> (\alpha --> \beta) )
+*   Rules : Modus Ponens 
+	If we have proofs of \alpha, \(alpha --> \beta) 
+        then we can derive \beta
+ 
+**  Example : proved (\alpha --> \alpha) in Hilbert's proof system.
+
diff --git a/class_15_11092023/summary.txt b/class_15_11092023/summary.txt
new file mode 100644
index 0000000..56450c5
--- /dev/null
+++ b/class_15_11092023/summary.txt
@@ -0,0 +1,11 @@
+Class 15 : Proofs with assumptions--inductive definition of provable formulas
+example : deriving \beta from assumptions {\alpha, (\neg \alpha))}.
+
+Monotonicity 
+Strong monotonicity 
+
+Deduction theorem
+Example : { (\alpha => \beta), (\beta => \gamma)} \derives (\alpha => \gamma)
+
+Proof of one direction of deduction theorem. 
+ 
diff --git a/class_16_12092023/summary.txt b/class_16_12092023/summary.txt
new file mode 100644
index 0000000..38ca0ae
--- /dev/null
+++ b/class_16_12092023/summary.txt
@@ -0,0 +1,13 @@
+Class 16 :  DT, Soundness, consistency
+
+Completion of proof of deduction theorem 
+Example proof of \derives (\neg \neg \alpha) --> \alpha
+
+Soundness theoreom : \Sigma \derives \alpha \implies \Sigma \entails \alpha 
+
+Consistency defn 1 : There does not exists a formula \alpha such that
+			\Sigma \derives \alpha and \Sigma \derives (\neg \alpha))
+Consistency defn 2 : There exists an alpha which is not derivable assuming \Sigma. 
+
+Thm: Equivalence of two notions of consistency. 
+
diff --git a/class_17_14092023/summary.txt b/class_17_14092023/summary.txt
new file mode 100644
index 0000000..5d127cb
--- /dev/null
+++ b/class_17_14092023/summary.txt
@@ -0,0 +1,20 @@
+Class 17 : Consistency, Satisfiability and Maximal consistency 
+
+Consistency of \emptyset using soundness
+
+Theorem : \Sigma is satisfiable ==> \Sigma is consistent
+
+Example (1) \Sigma_1=\{p\}
+Example (2) \Sigma_2=\{p_1,p_2,...\}
+Example (3) \Sigma_3=\{ p_i -> p_j | for all i,j\}
+Consistency of \Sigma іn the above examples using Theorem.
+
+Maximally Consistent Set (\Sigma): 
+(1) \Sigma is Consistent
+(2) \Sigma \derives \alpha OR \Sigma \union \{\alpha} is inconsistent
+
+Example (4) \Sigma_1 is consistent but not MCS
+Example (5) \Sigma_1 is consistent. Discussion of difficulty in
+proving it's maximal consistency. Motivation for the converse
+direction of above theorem. 
+
diff --git a/class_18_and_19_25and26092023/class_18_19_25_26092023.pdf b/class_18_and_19_25and26092023/class_18_19_25_26092023.pdf
new file mode 100644
index 0000000..376b8e5
Binary files /dev/null and b/class_18_and_19_25and26092023/class_18_19_25_26092023.pdf differ
diff --git a/class_18_and_19_25and26092023/summary.txt b/class_18_and_19_25and26092023/summary.txt
new file mode 100644
index 0000000..b64ed9c
--- /dev/null
+++ b/class_18_and_19_25and26092023/summary.txt
@@ -0,0 +1,9 @@
+Class 18 : \Sigma is consistent => \Sigma is satisfiable. 
+	 -- Construction of MCS from a consistent set 
+Class 19 : 
+	 -- proof of satisfiability of Maximal consistent set construted in the previous class. 
+            Thus completing the proof of consistency implies satisfiability  
+         -- Completeness Theorem for PL
+	 -- compactness theorem using completeness
+         -- maximal satisfiability Iff maximal consistency
+