Logic and Computation
CS 2800 Fall 2011

College of Computer and Information Science
Northeastern University
CS 2800 is a 4-credit course. The Office of the Registrar has useful information.

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.


Section 01: M,W,Th 10:30 AM-11:35 AM, International Village 019
Section 02: M,W,Th 4:35 PM-5:40 PM, International Village 019

For Instructors, TAs, and Tutors, click on Contact Info on your left.

The final schedule is:

You are required to check for announcements daily.


Books and Supplies

All that we require you to purchase is a TurningPoint Responder Card RF (also referred to as the TurningPoint clicker). You can purchase the card from the Northeastern University bookstore. Once you do, please log on to Blackboard and register the card. You can do that by logging in to the class, then clicking on Tools (on the left), and then find and click on the TurningPoint Registration Tool. You have to bring the card to every class.

There is no required book. If you want a reference that also includes a lot of exercises, then consider: Computer Aided Reasoning. Kaufmann, Manolios, Moore. You can order it from here. Please note that the book was written for at least upper level undergraduate students, so expect parts of the book to be hard. Also, in class we use a version of ACL2 that includes contracts and lots of other things that are not mentioned in the book. Nevertheless, this is the standard reference for ACL2 and contains many exercises whose solutions are available online. Use it as a reference and use it to supplement lectures.


We will be using the ACL2s system. Please download it and install it on your machines. It is also installed in the CCIS computer labs, but there are some instructions you should follow to use that installation properly.

Academic Integrity

Read and intimately familiarize yourselves with the Northeastern Academic Integrity policy.

Warning: We do not tolerate any violations. If we suspect that you violated the policy, we will report you and the consequences can be as severe as expulsion from the university.

For example, here is something you cannot do, but again, read the full policy.

Unauthorized Collaboration: The University defines unauthorized collaboration as instances when students submit individual academic works that are substantially similar to one another. While several students may have the same source material, the analysis, interpretation, and reporting of the data must be each individual's independent work.


There are 3 in-class exams which will take place on the following days: By popular request, here are copies of the exams we gave in Spring 2011. Notice that we had six exams that semester. The material covered in class changes from semester to semester, so please understand that there may be no relationship between the 2011 exams and the exams you get in class. Solutions are not provided. Work out the solutions yourselves and if you run into trouble, go to office hours.


The grading scheme for the class is based on video games. You will gain experience points by performing various tasks, including homework, quizzes, class participation, exams, and quests.

Grading Notes


CS 1800 and CS 2500
If you do not have this background you should get the permission of the instructor.