CSE 482 / CIS 582 : Logic in Computer Science. Fall 2005
Class: Tues/Thurs 1.303, Towne 309
Office hours: Wednesday 23 (Levine 609)
Topics covered in lectures
Homework 1; Solutions
Homework 2; Solutions
Course project, Due Nov 29
Homework 3; Solutions
Final: Dec 15, Noon2pm, Levine 307
Introduction
Logic has been called the calculus of computer science as it plays a
fundamental role in
computer science, similar to that played by calculus in the physical
sciences and traditional
engineering disciplines. Indeed, logic is useful in areas of computer
science
as disparate as architecture (logic gates), software engineering
(specification and verification),
programming languages (semantics, logic programming), databases
(relational algebra and SQL),
artificial intelligence (automatic theorem proving), algorithms
(complexity and expressiveness),
and theory of computation (general notions of computability).
CSE 482 provides the students with a thorough introduction to
mathematical logic, covering in
depth the topics of syntax, semantics, decision procedures, formal
proof systems, and soundness
and completeness for both propositional and firstorder logic. The
material is taught from a computer
science perspective, with an emphasis on algorithms, computational
complexity, and tools.
Projects will focus on problems in circuit design, specification and
analysis of protocols, and
query evaluation in databases.
Prerequisites
CSE 260 or equivalent
Grading
Grades will based on
 Homework Assignments (4 or 5)
 Midterm
 Final Exam
 Classroom Participation
 One Programming Project
Reading
The recommended text is
The lectures will not follow the text strictly.
Following books are recommended for additional reading
 A mathematical introduction to logic. Herbert Enderton,
Academic Press, 2nd Edition, 2001.
 Logic for Computer Science: Foundations of Automatic Theorem Proving,
Jean Gallier, Revised 2003 Edition available online
 Logic for Computer Scientists, Uwe Schoning, Birkhauser.
 Mathematical Logic for Computer Science,
Mordecai BenAri, Springer, 2nd Edition, 2001.
 Course notes of COMP 409 offered
by Prof. Moshe Vardi at Rice University.
Tentative Schedule
 Sept 8: Introduction
 Sept 13, 15, 20: Propositional logic: Syntax, semantics, expressiveness
 Sept 22, 27, 29: Proof systems; soundness and completeness
 Oct 4, 6: Review of complexity theory, NPcompleteness of propositional logic
 Oct 11, 13: Binary decision diagrams
 Oct 20: Resolution
 Oct 25: Horn clauses
 Oct 27: Midterm
 After midterm: Firstorder logic
 Final: Thursday, Dec 15, noon  2pm
Tools
Many tools allow declarative specifications using logic, and support powerful analysis based on optimized decision procedures. Here are links to sample tools:
 PVS: A stateoftheart automated theorem prover based on higherorder logic

SMV: The latest symbolic model checker for verification of finitestate reactive systems against temporal logic requirements
 Alloy: A firstorderlogicbased specification and analysis tool for software designs
Miscellaneous Links
Last updated on July 2005 by Rajeev Alur