CSE 482 / CIS 582 : Logic in Computer Science. Fall 2005
Class: Tues/Thurs 1.30-3, Towne 309
Office hours: Wednesday 2-3 (Levine 609)
Topics covered in lectures
Homework 1; Solutions
Homework 2; Solutions
Course project, Due Nov 29
Homework 3; Solutions
Final: Dec 15, Noon-2pm, 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 first-order 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 Ben-Ari, 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, NP-completeness of propositional logic
- Oct 11, 13: Binary decision diagrams
- Oct 20: Resolution
- Oct 25: Horn clauses
- Oct 27: Midterm
- After midterm: First-order 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 state-of-the-art automated theorem prover based on higher-order logic
-
SMV: The latest symbolic model checker for verification of finite-state reactive systems against temporal logic requirements
- Alloy: A first-order-logic-based specification and analysis tool for software designs
Miscellaneous Links
Last updated on July 2005 by Rajeev Alur