22c:188 (CS:4350)
Logic in Computer Science
The University of Iowa, Spring 2015
Schedule

Note: The schedule is tentative, including the due dates of homework assignments and the dates of the midterms. The cited references can be found in the Readings section.

The topics marked with (*) will not be part of the final exam, although you should have a rough idea of their motivation and connections to other relevant topics.

Date Topic Readings
Wed Jan 21
  • Course Introduction
  • Syllabus Overview
  • Logic as a Tool for Stating and Proving Arguments Formally
  • Types of Reasoning: Logic in CS is Deductive
Mon Jan 26
  • Declarative Statements: From Natural Language to Propositions
  • Syntax of Propositional Logic
  • A Natural Deduction Calculus for Propositional Logic
  • Some Rules of the Calculus
  • Examples of Derivations
  • Chap. 1, Sect 1-2 of [HR] (p1-10)
Wed Jan 28
  • More on the Rules of the Natural Deduction Calculus
  • Proofs and Nested Sub-proofs
  • Chap. 1, Sect. 2 of [HR] (p11-15)
Mon Feb 2
  • The Complete Set of Natural Deduction Rules
  • Chap. 1, Sect. 2 of [HR] (p15-23)
Wed Feb 4
  • Derived Inference Rules
  • Homework 1 out
  • Chap. 1, Sect. 2 of [HR] (p23-29)
Mon Feb 9
  • Truth Tables and Interpretations
  • Logical Entailment and its Properties
  • Relationship between Logical Entailment and Provability in Natural Deduction
  • Proof of Soundness of the Natural Deduction Calculus
  • Chap. 1, Sect. 4.4-5.1 of [HR] (p30-46)
Wed Feb 11
  • Proof of Soundness of the Natural Deduction Calculus (cont'd)
  • Proof of Completeness of the Natural Deduction Calculus
  • Homework 1 due
  • Chap. 1, Sect. 5.2 of [HR] (p46-50)
Mon Feb 16
  • Proof of Completeness of the Natural Deduction Calculus (cont'd)
  • Normal Forms and Validity and Satisfiability
  • Chap. 1, Sect. 5.2 of [HR] (p50-53)
Wed Feb 18
  • Equivalence Preserving Translation to Conjunctive Normal Form (CNF)
  • Satisfiability Preserving Translation to Conjunctive Normal Form (CNF)
Mon Feb 23
  • The DPLL Algorithm to Decide Satisfiability of Formulas in CNF
  • From DPLL to Conflict-driven Clause Learning (CDCL)
Wed Feb 25
  • The Need for More Expressive Logics
  • Introduction to First-Order Logic
  • Syntax of First-Order Logic
  • Chap. 2, Sect. 1 of [HR]
Mon Mar 2
  • Midterm I
  • All lectures up to and including Feb 23
  • Solutions of HW 1 on ICON
Wed Mar 4
  • Syntax of First-Order Logic (cont'd)
  • Substitutions
  • Chap. 2, Sect. 2 of [HR]
Mon Mar 9
  • Natural Deduction for First-Order Logic: Rules for Equality
  • Natural Deduction for First-Order Logic: Rules for Quantifiers
  • Chap. 2, Sect. 3 of [HR]
Wed Mar 11
  • Natural Deduction Proofs for First-Order Logic
  • Quantifier Equivalences
  • Chap. 2, Sect. 3 of [HR]
Mon Mar 16
  • Spring Break: no classes
Wed Mar 18
  • Spring Break: no classes
Mon Mar 23
  • Semantics of First-Order Logic
  • Homework 2 due
  • Chap. 2, Sect. 4 of [HR]
Wed Mar 25
  • Compactness Theorem for First-Order Logic
  • Limits to the Expressiveness of First-Order Logic
  • Higher-Order Logics
  • Chap. 2, Sect. 5-6 of [HR]
Mon Mar 30
  • Linear-Time Temporal Logic (LTL)
  • Transitions Systems as Models in Temporal Logic
  • Satisfaction of LTL Formulas on Computation Paths
  • Chap. 3, Sect. 1-2 of [HR]
Wed Apr 1
  • No Class
Mon Apr 6
  • Model Checking of LTL Formulas
  • Formalization in LTL
  • Chap. 3, Sect. 2 of [HR]
Wed Apr 8
  • Semantic Equivalences between LTL Formulas
  • Model Checking Example: A Mutual Exclusion Protocol
  • Chap. 3, Sect. 2.4-3.3.1 of [HR] (p184-190)
Mon Apr 13
  • Limits of Expressivity in LTL
  • Computation Tree Logic (CTL)
  • Syntax and Semantics of CTL
  • Model Checking with CTL
  • Project 1 due
  • Chap. 3, Sect. 4 of [HR]
Tue Apr 14
  • Homework 3 due
Wed Apr 15
  • Comparison of Expressivity of LTL and CTL
  • The Temporal Logic CTL*
  • Model Checking with NuSMV
Mon Apr 20
  • Midterm II
  • All lectures up to and including Apr 13
  • Solutions of HW 2 and HW 3 on ICON
Wed Apr 22
  • A Model Checking Algorithm for CTL
  • Ordered Binary Decision Diagrams
  • Overview of Symbolic Model Checking
  • Chap. 6, Sect. 1-3 of [HR]
  • Chap. 3, Sect. 6.1 of [HR]
Mon Apr 27
  • Modal Logics for Reasoning about Modes of Truth: Necessity, Knowledge, Belief etc.
  • Syntax and Semantics
  • Accessibility Relations and Kripke Models
  • Chap. 5 of [HR] (Sec. 1-2)
Wed Apr 29
  • Correspondence Theory
  • Properties of Kripke Frames and Valid Formulas
  • Defining Modal Logics Axiomatically
  • Examples of Other Modal Logics: T, S4 and S5
  • Chap. 5 of [HR] (Sec. 3)
Mon May 4
  • Natural Deduction for Modal Logics
  • Multi-modal Logics
  • Chap. 5 of [HR] (Sec. 4-5)
Wed May 6
  • Summary and Review
  • Course Evaluation
  • Homework 4 due
Mon May 11-
Fri May 15
  • Final Exam Week

22c:188 (CS:4350)
Logic in Computer Science
Spring 2015

Lectures

Every Monday and Wednesday 3.30pm-4.45pm in 218 MLH

Instructor

Dr. Christoph Sticksel
Email

Office hours in 201G MLH

  • Monday 5pm-6.30pm,
  • Wednesday 2pm-3.30pm, and
  • by appointment

Teaching Assistant

Md Hasib Bin Shakur
Email

Office hours in 101N MLH

  • Tuesday 5pm-6.30pm, and
  • Thursday 5pm-6.30pm.