CS2800: Logic and Computation - Syllabus
Fall 2010
[Main Page]
[Lectures]
[Assignments]
[Labs]
CS2800 is a 4-credit course. The corequisite lab portion, CS2801,
is a 1-hour course.
Prerequisites
You should have completed CS1800 and CS2500 before taking CS2800.
You should get approval from the instructor if you have not.
Course Description
Introduces formal logic and its connections to computer and
information science. Offers an opportunity to learn to translate
statements about the behavior of computer programs into logical
claims and to gain the ability to prove such assertions both by
hand and using automated tools. Considers approaches to proving
termination, correctness, and safety for programs. Discusses
notations used in logic, propositional and first order logic,
logical inference, mathematical induction, and structural
induction. Introduces the use of logic for modeling the range of
artifacts and phenomena that arise in computer and information
science.
Textbooks
We will use the following textbook:
Computer-Aided
Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother
Moore. Kluwer Academic Publishers, June, 2000. (ISBN: 0-7923-7744-3)
Note: An updated paperback version can be
purchased on the Web. This is much cheaper than the hardcover
version. Used copies might be available from students previously
in the class.
You may skip the following parts of the book, which will not be used/covered
in this course:
- Section 3.8, "Guards and Type Correctness"
- Section 3.9, "Introduction to Macros"
- Section 4.6, "Arrays and Single-Threaded Objects"
- Chapter 5, "Macros"
- Appendix sections A.1 - A.3 are largely irrelevant
Tentative Syllabus
Here is an overview of the material that we expect to cover. We
reserve the right to make modifications.
- The ACL2 programming language
- Data types
- Primitive functions
- Defining functions
- Common recursion schemes(idioms)
- Totality and Termination
- Tail recursion
- Multiple values
- Mutual recursion
- Formalizing pre and post conditions
- Testing
- Propositional Logic
- Basic connectives from a computational viewpoint
- Truth tables
- Satisfiability and validity
- Proof techniques (including case analysis, deduction law, instantiation)
- Equational reasoning
- Algorithmic considerations: completeness, exhaustive testing, decision procedures
- Using propositional logic to reason about programs
- The ACL2 logic
- Quantifier-free first order logic
- Specifying properties of programs
- Axioms of ACL2
- Substitution
- Equational Reasoning
- The definitional principle
- Termination
- Recursion and Induction
- Generalization
- Proving programs correct
- Quantification and its relation to recursion
- Algorithmic considerations: completeness, exhaustive testing, decision procedures
- Mechanization of ACL2
- Organization of ACL2
- Simplification
- Decision procedures
- Proof techniques
- The method
- Inspecting failed proofs
- Proof strategies and modularity
- Applications
- Data Structures
- Logic Design
- Compilers
- Video Games
- ...
Grading
- Homework (10% of your grade).
There will be regular homework assignments, usually turned
in via Blackboard.
For most homeworks, you will be allowed to work in teams
of 2. We recommend that you to first try to solve the
problems on your own, and then meet with your teammate to go
over your solutions and try to solve any unresolved
problems.
- Quizzes (3% of your grade)
Be prepared for a short quiz every day. Only a subset of the quizzes will be graded.
- Class participation
- 6 exams (14% each).
There will be no makeup exams,
for any reason. You can drop up to 2 exams. When we assign
grades, we will automatically determine which (if any) of the
exams it is to your advantage to drop.
You may use one double-sided (or two single-sided) cheat sheet
during each exam.
- Final exam (0-28%).
You can drop 0-2 exams and the final exam will count for the remainder of
your grade. You can also simply use the grades from your 6 exams and then
you do not need to take the final exam. You may use two double-sided
(or four single-sided) cheat sheets during the final.