Syllabus for CIS301: Logical Foundations of Computing

Textbook: The course uses an on-line text I have written, found at the web page, http://www.cis.ksu.edu/~schmidt/301s14/Lectures.

Course Structure and Grading: We meet for lecture Mon-Wed-Fri. There will be in-class drills as well as weekly homework exercises, where you use software tools to develop and check program and logic proofs. There will also be some small programs to write in Python and Prolog. Plan for two in-class quizzes, as well as a quiz during the scheduled Final-Exam period. Drills, exercises, and exam performances are added together to determine the final grade. Final letter 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 software evolved from circuits and symbolic logic, and we will see how every computer program contains a ``logical skeleton'' (like a electronic circuit's schematic) that forecasts the program's computation. We can use the logical skeleton as a mathematical proof of the program's correctness, just like you do in algebra or circuit-theory class. We will also study symbolic logic itself --- what it looks like, what it means, and how to manipulate it within formal proofs. Finally, we will learn useful 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. truth tables for analyzing simple circuits; algebra as a circuit-design language
2. deduction law for imperative assignment; program-correctness proofs in Floyd-Hoare style
3. deduction law for conditional (if) commands; logical properties of functions and procedures: pre- and post-conditions, global-variable invariants; invariants for functions that are recursively defined (call themselves).
4. deduction law for while-loops; loop invariants; mathematical induction
5. grammars and parsing; inductive definition of parse trees, parsers, and interpreters.
6. propositional logic in natural-deduction format; tactics for applying deduction laws; relation of the deduction laws to truth tables; normal forms and resolution theorem proving.
7. deduction laws for the quantifiers and their application to programs that manipulate data structures; first-order unification and its application in resolution theorem proving; introduction to soundness and completeness
8. logic programming in Prolog

Provost's requirements: Please read http://www.k-state.edu/provost/resources/teaching/course.html for the Provost's requirements regarding course structure and conduct.

Academic honesty policy: See 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 as well.

Academic accommodation for disabled students policy: If you have a physical or learning disability that requires special accommodation, please notify the Instructor as soon as possible.

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. February 25 is the last day to drop a course without a "W" recorded on your transcript; March 31 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.