Description
About the course
Professor S Arun Kumar, a faculty from the Department of Computer Science and Engineering at the Indian Institute of Technology, Delhi has designed this course. This course introduces logic as a tool for computer science. In this course, you will learn about the syntax and semantics of propositional logic, followed by logical and algebraic concepts, identities and normal forms. After that, you will learn about tautology checking, propositional unsatisfiability, analytic tableaux, consistency, and completeness. In addition to this, you will learn about the completeness theorem, maximally consistent sets, formal theories, and Hilbert-style proof theory. After that, you will learn about derived rules, the soundness and completeness of the Hilbert system.
Also, you will be introduced to introduction to predicate logic and its semantics, followed by substitutions, models, structures, and substructures. Then, you will understand the first order theories, and the proof theory of predicate logic along with existential quantification, normal forms, skolemization, substitutions, and instantiations. After that, you will understand about unification, resolution in fol, followed by its soundness and completeness. Next, the course will help you to learn about resolution and tableaux, completeness of tableaux method and Hilbert system. Finally, you will understand the first order theories, logic programming, verification of imperative programs and verification of while programs.
Learning Outcomes
After completing this course, you will be able to:
- Understand, explain and illustrate the meaning of given logical formulas, to translate such formulas into English and vice-versa.
- Express and formalize in logical language properties of models such as graphs, strings, and transition systems.
- Determine the truth or falsity of formulas in a given model.
- Boost your hireability through innovative and independent learning.
Target Audience
The course can be taken by:
Students: Students: All students who are pursuing professional graduate/post-graduate courses related to computer science and engineering or data science.
Teachers/Faculties: All computer science and engineering teachers/faculties.
Professionals: All working professionals from computer science / IT / Data Science domain.
Why learn Logic for CS?
Logic is essentially the study of reasoning or argumentation. We all use reason all the time to draw inferences that are useful to us. If our car would not start, we reason that the battery may be dead. So we test the battery. If the battery is not dead, then we deduce the problem must lie elsewhere, perhaps with the starter motor. So we check the starter motor. And so on. In this example the reasoning is simple, but sometimes chains of reasoning can become quite complicated.
Training ourselves to construct good arguments and to spot bad ones is a skill that is useful in just about every field as well as in everyday life. It helps steer us toward truth and away from falsehood. Logic is foundational to any field that makes use of arguments. It has especially close connections to mathematics, computer science, and philosophy. Both Aristotelian logic and modern symbolic logic are impressive bodies of knowledge that constitute major intellectual achievements. It is important to learn logic for computer science to build foundations of mathematical rigor that are used in most areas of Computer Science and limitations of Computation.
Course Features
- 24X7 Access: You can view lectures as per your own convenience.
- Online lectures: 32 hours of online lectures with high-quality videos.
- Updated Quality content: Content is latest and gets updated regularly to meet the current industry demands.
Test & Evaluation
There will be a final test containing a set of multiple choice questions. Your evaluation will include the scores achieved in the final test.
Certification
This course is free and it has no certificate.
Topics to be covered
- Module-1: Introduction
- What is Logic? (Open Video)
- What is Reasoning, Truth and Validity?
- What is Objectivity in Logic?
- What is Formal Logic?
- How to separate form and content and what are the facets of Mathematical Logic?
- Module-2: Propositional Logic Syntax
- How Logic and Computer Science are related?
- What is Truth and Falsehood?
- What is Propositional Logic Syntax?
- What is Precedence of Operators convention?
- Module-3: Semantics of Propositional Logic
- What is Syntactic identity?
- What are the Semantics of Propositional Logic and what is Truth Assignment?
- What is Tautology, Contradiction and Contingent?
- Module-4: Logical and Algebraic Concepts
- What is a Logical Consequence (part 1)?
- What is a Logical Consequence (part 2)?
- What is Logical Implication and Equivalent?
- What is Implication and Equivalence and how to determine whether a logical equivalence is a Congruence?
- Module-5: Identities and Normal Forms
- Recap of Logical Consequence, Implication and Equivalence.
- What are the various Logical Identities, what is adequacy and its example?
- What is the concept of functional completeness?
- What is the principle of Duality?
- What are Negation Normal Forms?
- Module-6: Tautology Checking
- How to check the validity and falsification of certain set of arguments?
- How to identify Atoms in Arguments and represent them?
- What is Propositional rendering?
- How checking of Tautology is carried out (part 1)?
- How checking of Tautology is carried out (part 2)?
- How checking of Tautology is carried out (part 3)?
- Module-7: Propositional Unsatisfiability
- What is Propositional Resolution?
- How to do clean-up to preserve logical equivalence?
- What is Resolution Method and its algorithm?
- Example of Resolution Method?
- Module-8: Analytic Tableaux
- What are the drawbacks of Resolution?
- What is Analytic Tableaux method and what are the basic Tableaux facts?
- What are the various Tableaux rules and what is the structure of rules?
- What is a Tableaux and its example?
- How to create a Slim Tableaux?
- Module-9: Consistency and Completeness
- How restructuring of the Tableaux rules is done?
- What is the notion of Consistency and Unsatisfiability?
- What is a Hintikka set?
- What is Hintikka's Lemma and what is the relation between Tableaux and Hintikka sets?
- What is Completeness?
- Module-10: The Compactness Theorem
- What is the Satisfiability of infinite sets?
- What are trees and what is Konig's lemma (part 1)?
- What are trees and what is Konig's lemma (part 2)?
- What is the Compactness Theorem (part 1)?
- What is the Compactness Theorem (part 2)?
- Module-11: Maximally Consistent Sets
- What are the consequences of Compactness theorem and what are consistent sets?
- What are the properties of a finite character?
- How to prove Tukey's Lemma?
- What are Maximally Consistent Sets and what is Lindenbaum's Theorem?
- Exercise on Konig's Lemma, Hintikka Sets, Tukey's theorem etc.
- Module-12: Formal Theories
- What is Reasoning?
- What is a proof system, its requirements and desirable properties?
- What is a formal theory (part 1)?
- What is a formal theory (part 2)?
- What is a Hilbert Style Proof System?
- Module-13: Proof Theory: Hilbert Style
- Recap of formal theory and Hilbert Style Proof System
- An Example proof
- What is a formal proof and what is the deduction theorem?
- What is the deduction theorem (continued part 1)?
- What is the deduction theorem (continued part 2)?
- Module-14: Derived Rules
- What are the derived rules?
- What is Sequent form, how proof trees are expressed in sequent form and what is transitivity of conditional?
- What are derived double negation rules?
- What are the derived operators and the rules for them?
- What is Gentzen's Natural Deduction System?
- Module-15: Hilbert System: Soundness
- What is the issue of incompleteness of formal theory?
- What is the consistency issue of a formal theory?
- What is the consistency of Hilbert System and notion of completeness?
- How to simulate Truth tables to prove a tautology?
- Module-16:The Hilbert System :Completeness
- What is the soundness of Hilbert System?
- What is the completeness theorem?
- What is the completeness theorem (continued)?
- Module-17: Introduction to Predicate Logic
- What is Predicate Logic (part-1)?
- What is Predicate Logic (part-2)?
- What is the syntax of Predicate Logic (part-1)?
- What is the syntax of Predicate Logic (part-2)?
- Module-18: The Semantic of Predicate Logic
- What are the semantics of Predicate Logic (part-1)?
- What are the semantics of Predicate Logic (part-2)?
- What are the semantics of Predicate Logic (part-3)?
- What are the semantics of Predicate Logic (part-4)?
- Module-19: Substitutions
- What is the Coincidence lemma for formulae (part-1)?
- What is the Coincidence lemma for formulae (part-2)?
- What is the notion of Syntactic substitutions?
- What is admissibility?
- What is the substitution lemma for formulae?
- Module-20: Models
- What is Logic and the notion of satidfiability?
- What are models and its examples?
- What is the notion of Logical Consequence and Validity?
- What are the negations of Semantical Concepts?
- What is the notion of Truth and Falsehood?
- Module-21: Strutures and Substructures
- What is the notion of Distinguishability?
- What are Isomorphic Structures and what is Isomorphism Lemma?
- What are Substructures and its examples (part-1)?
- What are Substructures and its examples (part-2)?
- What is the notion of Quantifier Formulae, Lemma for it and what are Universal and extential formulae?
- Module-22: First-Order Theories
- What is the Substructure Lemma?
- What is the Proof Theory of First Order Logic and Hilbert Style Proof System?
- Hilbert Style Proof System (continued)
- What is Predicate Logic?
- What is a faulty and correct proof and what is Predicate logic with equality?
- Module-23: Predicate Logic: Proof Theory (continued..)
- What are Hilbert Style proof rules and sequent forms?
- What is the case of Equality and what are the semantics of equality?
- What is Alpha Conversion?
- What is Deduction Theorem for Predicate Calculus?
- What are some useful corollaries for Deduction theorem?
- Module-24: Existential Quantification
- What is Existential Generalisation?
- What is Existential Elimination?
- What are the remarks and restrictions on Existential Elimination?
- Equivalence of Proofs
- Module-25: Normal Forms
- Highlights of Last lecture
- What are natural deductions, moving quantifiers and quantifier movement?
- What are Prenex Normal Forms and what is Conjunctive and Prenex Conjunctive Normal Form?
- What is Herbrand Algebra, its Terms and Models?
- What are Ground Quantifier-free Formulae for Herbrand Models and how to design this model?
- Proof of Herbrand Model.
- Module-26: Skolemization
- What is Skolemization?
- What is the notion of Skolem Normal Form and Scolen Conjunctive Normal Form?
- What is a Ground Instance and Herbrand's Theorem?
- What is the Herbrand Tree of Interpretations?
- What is the compactness of Sets of Ground Formulae?
- Module-27: Substitutions and Instantiations
- What is the compactness of Closed Formulae?
- What is the Lowenheim-Skolem theorem?
- What is Substitution and Instantiation theory (part-1)?
- What is Substitution and Instantiation theory (part-2)?
- Module-28: Unification
- What is Syntactic Unification?
- What is Unifiability and examples of Unification?
- What is the notion of Generality of Unifiers and what are the most general unifiers?
- What is the notion of Positions and Disagreement Set?
- Disagreement and Unifiability
- Module-29: Resolution in FOL
- Recapitulation (part-1)
- Recapitulation (part-2)
- What are the different terminologies of Clauses and Clauses of Ground Instance?
- What are the properties of Clauses and Resolution of FOL?
- What is Resolution of FOL (part-1)?
- Module-30: More on Resolution in FOL
- What is Resolution of FOL (part-2)?
- What are the different remarks on Resolution?
- Example of Resolution
- What is Refutation?
- Module-31: Resolution : Soundness and Completeness
- Highlights of previous lesson
- What is the Soundness of FOL resolution (part-1)?
- What is the Soundness of FOL resolution (part-2)?
- How to justify the completeness of FOL resolution (part-1)?
- How to justify the completeness of FOL resolution (part-2)?
- Module-32: Resolution and Tableaux
- What is the theorem of Completeness of resolution refutation for ground clauses?, resolution examples
- What is the Lifting lemma?
- How to proof theorem of Completeness of resolution refutation for ground clauses?
- What is Tableaux method?
- What are various Tableaux rules?, tableaux example
- Tableaux example (continued)
- Module-33: Completeness of Tableaux Method
- What is the issue related with tableaux rule?
- What is First-order tableaux and its example?, what is Hintikka set and first-order hintikka sets?
- What is Hintikka lamma for FOL?, what is the Hintikka theorem for first order tableaux?
- What is the Soundness and completeness of first-order tableaux?, Assignment
- Module-34: Completeness of the Hilbert System
- How to proof Completeness of the Hilbert System (part-1)?
- How to proof Completeness of the Hilbert System (part-2)?
- How to proof Completeness of the Hilbert System (part-3)?
- How to proof Completeness of the Hilbert System (part-4)?
- Module-35: First -Order Theories
- What is the theory of Directed and Undirected graphs?
- What is the theory of Irreflexive partial orderings?, what is the theory of Irreflexive linear orderings?
- What is the notion of Reflexive preorders, Reflexive partial orderings and Equivalence relations?
- What is the Peano's postulates theory?
- What is the theory of Naturals?
- What is the theory of Naturals (continued)
- Module-36: Towards Logic Programming
- Highlights of previous lesson
- How to reverse the arrow?, what is Horn clauses , goal claues and logic programs?
- Why logic programs is important?
- How to do sorting in logic programs?
- How to do sorting in logic programs (continued)?
- Use of Prolog
- Module-37: Verification of Imperative Programs
- How to define While programming language?
- How to While loop execute?
- How to define semantics of while?
- How programs are define as predicate transformers?, what is the total correctness of programs?
- What are the Proof rules for partial correctness?
- Module-38: Verification of WHILE Programs
- Factorial example
- What are the Proof Rules?
- What is the concept of Total correctness?, what are the termination rules?
- How to proof factorial example (part-1)?
- How to proof factorial example (part-2)?
- Logic for CS - Final Quiz
Note : Parts of this material has been sourced from NPTEL, adapted and modified to adhere to our Pedagogical requirements and uploaded to YouTube for reuse under the same license.
Reviews
There are no reviews yet.