Class Logs and Assigned Readings
The cited references can be found in the Readings section.
| Date | Topics | Readings |
|---|---|---|
| 01/16/07 |
Course introduction and syllabus overview. Discussion of the basic role of Symbolic Logic in Computer Science: logic as the formal foundation of CS. Basic components of a logic: syntax, semantics and inference rules. Logic as a tool for stating and proving arguments formally. |
- [Var] (Suggested) - [VK] (Suggested) |
| 01/18/07 |
Introduction to propositional logic. Scope of the logic. The language: propositional symbols and connectives. A natural deduction-style calculus. Rule of the calculus. Examples of formal proofs in the calculus. |
- Chap. 1 of [HR] |
| 01/23/07 |
More on the rules of the natural deduction calculus.
Proofs and nested subproofs.
More examples. Formal definition of the language of PL. Formal semantics of PL formulas. Truth tables and interpretations. Compositional nature of the PL semantics. |
- Chap. 1 of [HR] |
| 01/25/07 |
Satisfiable, unsatisfiable, valid and invalid formulas.
Interpretations and models. The logical entailment relation |= and its properties. Examples. Logical equivalence. Examples of logically equivalent formulas. Relationship between logical entailment and provability in the natural deduction calculus. Soundness and completeness of the calculus. Proof of soundness. |
- Chap. 1 of [HR] - [Tin] |
| 01/30/07 |
Completion of soundness proof for the natural deduction calculus. Proof of completeness. |
Chap. 1 of [HR] |
| 02/01/07 |
Completion of completeness proof for the natural deduction calculus.
Significance of the calculus' soundness and completeness. Decidability of logical entailment in propositional logic. Alternative methods to check for logical entailment. Introduction to equivalence preserving transformations into a formal form. |
Chap. 1 of [HR] |
| 02/06/07 |
Conjunctive Normal Forms. A general, equivalence preserving, CNF conversion procedure. Examples or conversions. Checking the validity of PL formulas by conversion into CNF. Examples. Discussion on the complexity of equivalence preserving transformations into CNF. |
Chap. 1 of [HR] |
| 02/08/07 |
CNFs as compact representations of truth tables. Horn formulas. Definition and usage. A linear algorithm for deciding the satisfiability of Horn formulas. Examples. Introduction to efficient solvers for propositional satisfiability. |
Chap. 1 of [HR] |
| 02/13/07 |
Discussion of Homework 1 solutions. The DPLL procedure: main idea and applications. Abstract description of DPLL by mean of a transition system. The rules of the systems. Examples of applications and strategies. |
[Tin2] |
| 02/15/07 |
Improvements to the original DPPL procedure:
backjumping, learning and restarts. Motivations, discussion and examples. Termination and correctness of the DPLL system with backjumping. Termination and correctness of the DPLL system extended with learning and restarts with backjumping. Introduction to temporal logic. |
[Tin2] |
| 02/20/07 | Midterm I | See Exams section |
| 02/22/07 |
Linear temporal logic.
Syntax and semantics. Motivation and applications. Definition and discussion of the satisfiability relation betwen paths and LTL formulas. |
Sec. 3.1, 3.2 of [HR] |
| 02/27/07 |
Definition and discussion of the satisfiability relation betwen states and LTL formulas. Examples of transition systems. Examples of formulas and paths that falsify/satisfy them. Brief discussion of Midterm I. |
Sec. 3.2 of [HR] |
| 03/01/07 |
More sample solutions for Midterm I. Semantical equivalence in LTL. Examples of equivalent LTL formulas. Defining temporal operators in terms of others. Minimal subsets of temporal operators. |
Sec. 3.2 of [HR] |
| 03/06/07 | Practice with LTL. Modelling a simple transition system, specifying properties of the system in English, translating them into LTL formulas, and manually verifying the satisfiability of those formulas in the system. | Sec. 3.2 of [HR] |
| 03/08/07 |
Applications of LTL: a mutual exclusion protocol.
Modelling a two-process system; specifying properties such as safety, liveness and so on;
verifying then manually against the model. Brief discussion of applications of LTL in the hardware and software industry, and of model checking tooks like NuSMV. Limits on the expressive power of LTL. Introduction to branching time logics and to CTL. |
Sec. 3.3, 3.4 of [HR] |
| 03/13/07 | Spring break | |
| 03/15/07 | Spring break | |
| 03/20/07 |
Syntax and semantics of CTL.
Comparisons with LTL.
Modeling English specifications into CTL.
Examples of satisfiable/unsatisfiable CTL formulas in a given state of a model. Equivalence of CTL formulas. Significant examples. |
Sec. 3.4 of [HR] |
| 03/22/07 |
More examples of equivalent CTL formulas. Defining the additional temporal operators A[_R_], E[_R_], A[_W_], and E[_W_] in terms of existing ones. Discussion of Homework 4. An algorithm for checking the satisfiability of CTL formulas in a state. |
Sec. 3.4 of [HR] |
| 03/27/07 | No class | |
| 03/29/07 | Midterm II | See Exams section |
| 04/03/07 | More on the model checking algorithm for CTL formulas. Pseudo-code presentation and simulation on various examples. | Sec. 3.4 of [HR] |
| 04/05/07 | Binary Decision Diagrams. Introduction and motivation. Applications of BDDs for CTL model checking. From decision trees to decision diagrams. Reduced BDDs. The reduction rules. Ordered BDDs. Canonical representations. | Sec. 6.1 of [HR] |
| 04/10/07 | More on Ordered BDDs. Building OBDDs from formulas. Algorithms for reduced OBDDs. Combining OBDDs. The apply procedure. Examples. Computational complexity of main operations. | Sec. 6.1-6.2 of [HR] |
| 04/12/07 | Further operations on OBDDs: restrict and exists. Introduction to BDD-based symbolic model checking. Representing sets and set operations with OBBDs. Encodings and examples. | Sec. 6.2-6.3 of [HR] |
| 04/17/07 | Representing CTL models with BDDS. Different encodings of the transition relations. Examples. | Sec. 6.3 of [HR] |
| 04/19/07 |
Introduction to the Mu-calculus.
Syntax. Intuition behind the &mu and &nu binders. Discussion of Midterm II solutions. |
Sec. 6.4 of [HR] |
| 04/24/07 |
More discussion on the Midterm II solutions. Semantics of the Mu-calculus and examples of valuations. Translating CTL formulas into Mu-calculus formulas. General translation and examples. |
Sec. 6.4 of [HR] |
| 04/26/07 |
Modal logics, introduction and motivation.
Modalities and their use to reason about necessity, time, knowledge, belief, etc.
Connections to temporal logics. The basic modal logic K. Syntax and semantics. Accessibility relations and Kripke models. Validity and valid formulas in K. |
Sec. 5.1 -- 5.3 of [HR] |
| 05/01/07 |
Kripke frames.
Correspondence theorems modal logics.
Samples and a proof. Defining modal logics axiomatically. A modal logic to reason about knowledge: KT45. |
Sec. 5.4 of [HR] |
| 05/03/07 | More on reasoning about knowledge. The wise-men puzzle. Discussion and formalization in KT45. | Sec. 5.4 of [HR] |
| 05/08/07 | Final exam | See Exams section |