Syllabus for CIS301: Logical Foundations of Computing

Textbook: The course uses an on-line text I have written, found at the Lectures page at http://www.cis.ksu.edu/~schmidt/301f09. There is an optional course text, 2d Edition: Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan, Cambridge Univ. Press. During the second half of the course, we will cover the material in Chapters 1 and 2. The book is expensive and is not required.

Course Structure: We meet for lecture Mon-Wed-Fri; Friday is typically ``exercises day''; there will be weekly exercises and three in-class written exams. The exercises will be a mix of pencil-and-paper and tool-checking activities. There will also be one or two programming assignments. Final grades are not based on strict percentage cutoffs but are ``curved'' by taking into account the difficulty of the exercises and exams.

Prerequisites: CIS200 or equivalent experience. Please see the instructor if you have questions. A computer is not required for the course; you may do the computerized exercises in any of the KSU labs.

Objectives and Topics: We will learn how circuits and software are based on symbolic logic, and we will use logic to reason about the design and correctness of both. We will also study symbolic logic itself --- what it looks like, what it means, and how to manipulate it within formal proofs. As time allows, we will learn useful programming techniques that you are unlikely to see elsewhere based on grammars, dynamic data structures, and logic programming.

Here is a summary of the topics covered:

1. boolean operators and truth tables for analyzing simple circuits; equations as a circuit-design language; algebraic laws for equational systems
2. forwards and backwards deduction laws for imperative assignment; laws for conditional (if) commands; deducing logical properties of imperative programs
3. logical properties of functions and procedures: pre- and post-conditions, global-variable invariants; invariants for functions that are recursively defined (call themselves). Semantics of recursively defined data structures (e.g., trees) and the functions that process them. Grammars and parsing.
4. deduction law for while-loops; loop invariants; simple examples of quantification; mathematical induction
5. propositional symbolic logic in natural-deduction format; tactics for applying deduction laws; soundness and completeness: relation of the deduction laws to truth tables and lattice-theoretic models; application to program proving; resolution theorem proving.
6. logical laws for the quantifiers and their application to programs that manipulate data structures; more mathematical induction; first-order unification and resolution theorem proving; logic programming in Prolog.
7. Application of logic to programming-by-contract; introduction to linear-time temporal logic and its application to multi-component systems (if time allows).

Academic honesty policy: Please read http://www.ksu.edu/Honor for the University's policy regarding academic honesty. The weekly exercises are meant to develop your skills; it is OK to discuss them with others and to ask for help with the tricky bits, but what you submit must be written/typed by you, and you must be able to reproduce it from memory, from scratch, whenever asked. That is, whatever you submit must be saved in your brain.

Attendance policy: You are responsible for the material presented during the lectures. If you miss a lecture, consult a fellow student or the instructor to learn what you missed. Attendance is required on Exercise Days (typically, Fridays).

Drop policy: It is your responsibility to drop the course if you are enrolled but decide not to complete the course --- there are no ``automatic'' drops due to nonattendance. September 28 is the last day to drop a course without a "W" recorded on your transcript; October 30 is the last day to drop a course (with a "W"). KSU allows a retake of a course with removal of the prior grade, at most once per course, for a maximum of five courses.

Academic accommodation for disabled students policy: If you have a physical or learning disability that requires special accommodation, please notify the Instructor within the first two weeks of the course.