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, SH 305
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.

Final Exam Schedule:

• Sections 01 and 02, Manolios and Wahl, April 23, 3:30-5:30PM in MU (Mugar Life Sciences Building) 201.

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:

• Monday, Feb 11
• Thursday, March 14
• Thursday, April 11

To help you prepare for exams, here are copies of the exams we gave in Spring 2012. The material covered in class changes from semester to semester, so please understand that there may be no relationship between the 2012 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

Grading

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

• Homework (2000 experience points).
  There will be weekly homework assignments. You will mostly work in groups. You can only work with students in your group. Group members can be different sections. 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 10PM, unless otherwise noted.
• Labs (600 experience points).
  During lab, the TAs and tutors will review the weekly material by giving you problems to work on. They will check your solutions, ask you to present solutions, answer questions, and provide solutions. Think of labs as tutoring sessions. They are intentionally small so that you can get individualized, personalized attention. Take advantage of this by coming prepared and being as engaged as possible.

• Quizzes and Class Participation (1400 experience points).
  Be prepared for a short quiz every day. Quizzes and class participation will utilize the TurningPoint clicker. We may 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 (2000 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 (2000 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.
• The total available points shown above are 10,000. Your grade will be determined by the number of experience points you obtain. Here are the cutoffs.

  A	A-	B+	B	B-	C+	C	C-	D+	D	D-
  9300	9000	8700	8300	8000	7700	7300	7000	6700	6300	6000

• Quests.
  During the semester, we will give you side quests that you can tackle by forming guilds. Quests are optional and are intended to be challenging.
  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.

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 homework 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.