Propositional Logic : Syntax, Unique parsing, Semantics, Equivalences, Consequences, Calculations, Informal proofs.

Normal Forms and Resolution : Clauses, CNF and DNF representations, Adequacy of calculations, SAT, Resolution refutation, Adequacy of resolution.

Proof Systems : Axiomatic system PC, Adequacy of PC, Analytic tableau PT, Adequacy of PT, Compactness of PL.

First Order Logic : Syntax of FL, Scope and binding, Substitutions, Semantics of FL,Quantifier laws, Equivalences, Consequences.

Normal Forms in FL : Calculations, Informal proofs, Prenex forms, Skolem forms,Herbrand’s theorem, Skolem-Lowenheim theorem, Resoltion in FL.

Proof Systems for FL : Axiomatic system FC, Analytic tableau FT, Adequacy of FC and FT, Compactness in FL.
Axiomatic Theories : Undecidabilty of FL, Godel’s incompleteness theorems.

Other Resources

Course Curriculum

Mod-01 Lec-01 Sets and Strings Details 44:21
Mod-01 Lec-02 Lecture-02-Syntax of Propositional Logic Details 45:55
Mod-01 Lec-03 Lecture-03-Unique Parsing Details 52:14
Mod-01 Lec-04 Lecture-04-Semantics of PL Details 47:5
Mod-01 Lec-05 Lecture-05-Consequences and Equivalences Details 44:12
Mod-01 Lec-06 Five results about PL Details 40:51
Mod-01 Lec-07 Lecture-07-Calculations and Informal Proofs Details 46:24
Mod-01 Lec-08 Lecture-08-More Informal Proofs Details 48:25
Mod-01 Lec-09 Lecture-09-Normal forms Details 50:42
Mod-01 Lec-10 Lecture-10-SAT and 3SAT Details 45:32
Mod-01 Lec-11 Lecyture-11-Horn-SAT and Resolution Details 55:5
Mod-01 Lec-12 Lecture-12-Resolution Details 47:21
Mod-01 Lec-13 Lecture-13-Adequacy of Resolution Details 53:27
Mod-01 Lec-14 Lecture-14-Adequacy and Resolution Strategies Details 48:34
Mod-01 Lec-15 Lecture-15-Propositional Calculus (PC) Details 49:50
Mod-01 Lec-16 Lecture-16-Some Results about PC Details 48:54
Mod-01 Lec-17 Lecture-17-Arguing with Proofs Details 47:3
Mod-01 Lec-18 Lecture-18-Adequacy of PC Details 51:6
Mod-01 Lec-19 Lecture-19-Compactness & Analytic Tableau Details 49:44
Mod-01 Lec-20 Lecture-20-Examples of Tableau Proofs Details 45:10
Mod-01 Lec-21 Lecture-21-Adequacy of Tableaux Details 45:44
Mod-01 Lec-22 Lecture-22-Syntax of First order Logic (FL) Details 47:11
Mod-01 Lec-23 Lecture-23-Symbolization & Scope of Quantifiers Details 48:28
Mod-01 Lec-24 Lecture-24-Hurdles in giving Meaning Details 45:34
Mod-01 Lec-25 Lecture-25-Semantics of FL Details 50:16
Mod-01 Lec-26 Lecture-26-Relevance Lemma Details 48:2
Mod-01 Lec-27 Lecture-27-Validity, Satisfiability & Equivalence Details 49:12
Mod-01 Lec-28 Lecture-28-Six Results about FL Details 48:10
Mod-01 Lec-29 Lecture-29-Laws, Calculation & Informal Proof Details 47:23
Mod-01 Lec-30 Lecture-30-Quantifier Laws and Consequences Details 49:30
Mod-01 Lec-31 Lecture-31-More Proofs and Prenex Form Details 51:19
Mod-01 Lec-32 Lecture-32-Prenex Form Conversion Details 46:39
Mod-01 Lec-33 Lecture-33-Skolem Form Details 53:11
Mod-01 Lec-34 Lecture-34-Syntatic Interpretation Details 50:34
Mod-01 Lec-35 Lecture-35-Herbrand’s Theorem Details 45:12
Mod-01 Lec-36 Lecture-36-Most General Unifiers Details 50:45
Mod-01 Lec-37 Lecture-37-Resolution Rules Details 46:19
Mod-01 Lec-38 Lecture-38-Resolution Examples Details 49:21
Mod-01 Lec-39 Lecture-39-Ariomatic System FC Details 46:35
Mod-01 Lec-40 Lecture-40-FC and Semidecidability of FL Details 48:44
Mod-01 Lec-41 Lecture-41-Analytic Tableau for FL Details 47:30
Mod-01-Lec-42 Lecture-42-Godels Incompleteness Theorems Details 48:17

This course is part of NPTEL online courses, delivered by IIT Madras.

Course Reviews


  • 5 stars0
  • 4 stars0
  • 3 stars0
  • 2 stars0
  • 1 stars0

No Reviews found for this course.


FreeVideoLectures Provides you complete information about best courses online, Video tutorials, helps you in building a career !!

Learn More About us

About Us
Privacy Policy

top All rights reserved.

Setup Menus in Admin Panel