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 12 of [HR] (p110)

Wed Jan 28 
 More on the Rules of the Natural Deduction Calculus
 Proofs and Nested Subproofs

 Chap. 1, Sect. 2 of [HR] (p1115)

Mon Feb 2 
 The Complete Set of Natural Deduction Rules

 Chap. 1, Sect. 2 of [HR] (p1523)

Wed Feb 4 
 Derived Inference Rules
 Homework 1 out

 Chap. 1, Sect. 2 of [HR] (p2329)

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.45.1 of [HR] (p3046)

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] (p4650)

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] (p5053)

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 Conflictdriven Clause Learning (CDCL)


Wed Feb 25 
 The Need for More Expressive Logics
 Introduction to FirstOrder Logic
 Syntax of FirstOrder Logic


Mon Mar 2 

 All lectures up to and including Feb 23
 Solutions of HW 1 on ICON

Wed Mar 4 
 Syntax of FirstOrder Logic (cont'd)
 Substitutions


Mon Mar 9 
 Natural Deduction for FirstOrder Logic: Rules for Equality
 Natural Deduction for FirstOrder Logic: Rules for Quantifiers


Wed Mar 11 
 Natural Deduction Proofs for FirstOrder Logic
 Quantifier Equivalences


Mon Mar 16 


Wed Mar 18 


Mon Mar 23 
 Semantics of FirstOrder Logic
 Homework 2 due


Wed Mar 25 
 Compactness Theorem for FirstOrder Logic
 Limits to the Expressiveness of FirstOrder Logic
 HigherOrder Logics

 Chap. 2, Sect. 56 of [HR]

Mon Mar 30 
 LinearTime Temporal Logic (LTL)
 Transitions Systems as Models in Temporal Logic
 Satisfaction of LTL Formulas on Computation Paths

 Chap. 3, Sect. 12 of [HR]

Wed Apr 1 


Mon Apr 6 
 Model Checking of LTL Formulas
 Formalization in LTL


Wed Apr 8 
 Semantic Equivalences between LTL Formulas
 Model Checking Example: A Mutual Exclusion Protocol

 Chap. 3, Sect. 2.43.3.1 of [HR] (p184190)

Mon Apr 13 
 Limits of Expressivity in LTL
 Computation Tree Logic (CTL)
 Syntax and Semantics of CTL
 Model Checking with CTL
 Project 1 due


Tue Apr 14 


Wed Apr 15 
 Comparison of Expressivity of LTL and CTL
 The Temporal Logic CTL*
 Model Checking with NuSMV


Mon Apr 20 

 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. 13 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. 12)

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


Mon May 4 
 Natural Deduction for Modal Logics
 Multimodal Logics

 Chap. 5 of [HR] (Sec. 45)

Wed May 6 
 Summary and Review
 Course Evaluation
 Homework 4 due


Mon May 11 Fri May 15 


22c:188 (CS:4350)
Logic in Computer Science
Spring 2015
Lectures
Every Monday and Wednesday 3.30pm4.45pm in 218 MLH
Instructor
Dr. Christoph Sticksel
Email christophsticksel@uiowa.edu
Office hours in 201G MLH
 Monday 5pm6.30pm,
 Wednesday 2pm3.30pm, and
 by appointment
Teaching Assistant
Md Hasib Bin Shakur
Email mdhasibbinshakur@uiowa.edu
Office hours in 101N MLH
 Tuesday 5pm6.30pm, and
 Thursday 5pm6.30pm.