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.

Sections

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:

• Sections 01 and 02, Manolios and Wahl, April 23, 3:30-5:30PM in Richards Hall 200.

You are required to check for announcements daily.

Rules

• No electronic devices (computers, recording devices, phones, etc) in class without permission first. The only exception is your TurningPoint clicker. Bring that with you every day.
• If you don't understand something, please ask questions. We love questions. One of the benefits of attending a university as opposed to reading a book is that you get to interact with faculty.
• Keep it real. Tell me what works; what doesn't. What you like; what you don't like.
• We have clear policies that everyone needs to understand and adhere to. For example, late homeworks will not be accepted under any circumstances. If you ask us to make an exception for just you, the answer will be no: everybody plays by the same rules. Notice that you can question the policies themselves and if you make good suggestions, that may lead to changes in our policies.

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.

Software

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.

Exams

There are 3 in-class exams which will take place on the following days:

• Thursday, Feb 9
• Thursday, March 15
• Thursday, April 12

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.

• Exam 1
• Exam 2
• Exam 3
• Exam 4
• Exam 5
• Exam 6

Grading

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.

• Homework (1200 experience points).
  There will be weekly homework assignments. You will mostly work in groups. You can only work with students that are in the same lab as you; they can be in a different section. We will give you instructions on group sizes and composition. We recommend that you to first try to solve the problems on your own. Then meet with your teammate to go over your solutions and try to solve any unresolved problems. We will only grade a subset of the problems assigned. Homeworks will be due on Tuesday at 5PM, unless otherwise noted. The final few homeworks will be part of an end-of-semester project.
• Labs (240 experience points).
  Most of the time in lab will be devoted to code and proof walk-throughs. Every team will either defend or question. A team that is defending will be prepared to answer questions about their homework submission. The questions will be prepared by the questioning team, which will have access to the presenting team's submission in advance. Teams will alternate between questioning and presenting at weekly intervals. Both defending and questioning teams will be awarded experience points by the TAs. The better they do, the more points they get. In addition, the whole lab gets to vote on which team defended best, questioned best, and which pair of teams had the best interactions. All of these teams will get extra experience points. Ties will be broken by the TAs. Please read the detailed lab instructions for students.
• Quizzes and Class Participation (1200 experience points).
  Be prepared for a short quiz every day. Quizzes and class participation will utilize the TurningPoint clicker. We will only grade a subset of the quizzes given. If you are not present for a quiz or if you do not have your clicker, you will get 0 points.
• Exams (1200 experience points each).
  There will be no makeup exams, for any reason. However, you can drop 1 exam. When we assign grades, we will automatically determine which (if any) of the exams it is to your advantage to drop.
• Final exam (1200 experience points).
  If you are happy with your experience points from your exams, there is no need to take the final. If not, the final can replace one of your exam experience points.
• Quests (600 experience points).
  During the semester, we will give you side quests that you can tackle by forming guilds. The more difficult the challenge, the larger the guild you can form.
  Here are the rules for quests.
  • You can form a guild of up to the size specified for the quest.
  • You have to submit your solutions by the deadline specified for the quest.
  • You cannot discuss the quest with anyone besides the members of your guild.
  • You have to follow whatever other quest-specific instructions are given.
  • You must submit exactly one solution per guild. Every guild should have one guild member who submits a file with the filename questi where i is the quest number. This file should be commited to the repository in the student's directory (in Student/ccis_login). The file should start by indicating who the guild members are.
  • Once we check quest submissions, we will award experience points on Blackboard. We will be much stricter in the allocation of experience points than we are with homework. The idea is that you either complete your quest or you do not. Unless you made some minor mistake, do not expect to get any points for partial solutions.
• Your grade will be determined by the number of experience points you obtain, as follows.

  A	6000 or more points
  A-	5700-5999 points
  B+	5400-5699 points
  B	5150-5399 points
  B-	4900-5149 points
  C+	4650-4899 points
  C	4450-4649 points
  C-	4250-4449 points
  D+	4050-4249 points
  D	3900-4049 points
  D-	3750-3899 points
  F	0-3749 points

Grading Notes

• You can take 1 double-sided sheet of paper to each exam and to the final.
• You have exactly 1 week after any assignment, quiz, or exam is graded to challenge the experience points awarded. After that, we will not change your points.
• You are responsible for making sure that we entered the right points on Blackboard. If you notice any data entry errors, please inform us right away.
• You must take all exams and quizzes in the section you are registered for. If you take an exam or a quiz in a different section that the one you are registered for, you will not get any points for that exam or quiz.

Prerequisites

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