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.


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.


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:

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
  2. Propositional Logic
  3. The ACL2 logic
  4. Mechanization of ACL2
  5. Applications