In this module, you will learn about the symbolic manipulation technique of natural deduction. The module will also discuss the different rules of natural deduction with examples.

In this module, you will learn about state-of-the-art methods of resolution and Davis-Putnam-Logemann-Loveland (DPLL) methods to argue about the satisfiability of a propositional logic formula. We study the relevant characteristics of a logical theory, i.e., the consistency, soundness, and completeness, and comment on natural deduction as a proof technique on how it scores over these characteristics.

In this module, you will be introduced to model-based formal verification techniques, in particular, the model checking techniques. The module will informally discuss two popular families of temporal logics: linear temporal logic (LTL) and computation tree logic (CTL).

In this module, you will formally learn the LTL and CTL temporal logics. The module will also introduce you to the algorithms used for model checking over these algorithms. The module will further explain fundamental system properties, such as invariance, safety, and liveliness. Furthermore, the module will give provide you insight into how to encode natural language sentences into LTL and CTL formulas.

In this module, you will learn the need for predicate logic and how to express statements in predicate logic. You will also learn about the syntax of predicate logic and the fundamentals behind writing proofs in predicate logic. You would also learn the concept of substitution and the difference between the free variables and bound variables. You will also get introduced to basic predicate logic rules that are used for proving sequents.

In this module, you will learn to apply the proof rules of natural deduction to prove sequents in predicate logic. The proof rules that you would learn include: Universal Quantifier Elimination, Existential Quantifier Introduction, Universal Quantifier Introduction and Existential Quantifier Elimination. You would also learn to identify which specific rules to apply for writing proof of a given sequent.

In this module, you will learn about semantics and model interpretations in predicate logic. You would also learn about the satisfiability and validity of predicate logic formulas, along with the undecidability of validity. You would also learn about the limitations of first-order predicate logic and how second-order predicate logic is useful in such cases.

In this module, you will learn how to formally verify programs written in imperative style. More specifically, you will learn formal methods to verify assignment statements, sequence of statements, conditional statements, and iterative statements. You will also learn the formal method to verify whether a given program terminates or not.

In this module, you will learn to prove the total correctness of various commonly used algorithms such as computing the power of two numbers, finding an element from an unsorted array, and selection sort. You would also learn to deduce loop invariants for programs of the above computational problems and prove that these programs terminates.