# CS U290: Logic and Computation - Syllabus Fall 2008 (archived)

[Main Page] [Lectures] [Assignments]

CS U290 is a 4-credit course. The corequisite lab portion, CS U291, is a 1-hour course.

You should have completed CS U200 and CS U211 before taking CS U290. 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.
1. The ACL2 programming language
• Data types
• Primitive functions
• Defining functions
• Common recursions
• Tail recursion
• Multiple values
• Mutual recursion
• Assertions and testing
2. The ACL2 logic
• Quantifier-free first orer logic
• Axioms of ACL2
• Equational Reasoning
• Recursive definitions and the definitional principle
• Induction
• Quantification
• Termination
• Godel's completeness theorem
3. Mechanization of ACL2
• Organization of ACL2
• Simplification
• Decision procedures
• Proof techniques
• The method
• Inspecting failed proofs
• Proof strategies and modularity
4. 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.
• 6 exams (15% 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-30%).
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.