Logic and Computation
CS 2800 Spring 2014

College of Computer and Information Science
Northeastern University

Syllabus

CS 2800 is a 4-credit course.

Course Description

Introduces basic mathematical logic and its connections to computer science. Discusses concepts in (mostly propositional) logic, logical inference, mathematical induction, and structural induction. Introduces the use of logic for modeling a range of artifacts and phenomena that arise in computer 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 claims both on paper and using automated tools. Program properties considered include safety, termination, and general (functional) correctness.

Prerequisites
CS 1800 ("Discrete Structures") and CS 2500 ("Fundies I"). If you do not have this background, you must get the permission of the instructor.


Class Times and Location

Mon, Wed, Thu, in two sections, International Village 019


Rules of Conduct

No electronic devices (computers, recording devices, phones, etc).

Class meetings will be highly interactive. If you don't understand something, ask questions. If you go over the material at home and still something doesn't make sense, use one of the several options to follow up: Piazza (see below), office hours, email (last resort). Try these options in this order until you succeed. Don't give up.


Communication

We will be using Piazza, a Q&A platform, for most communication in this class. This includes announcements from our side (therefore, you must check Piazza daily) and class discussion that is deemed to be of general interest. Such discussion may concern class material, homework clarifications, but also any general comments on what you like about the class, and what you don't like. Please avoid email for these purposes.

For any personal issues that require privacy, you can send an email to the instructor or the TA. Likewise, you may choose to post a private note on Piazza, in which case it will be visible to all instructors. We promise that in such cases, any reply will be private, too.


Software

We will be using ACL2s (for "ACL2 Sedan"), a version of the ACL2 Theorem Prover. Please download ACL2s and install it on your machines. The ACL2s website contains detailed installation instructions. We will practice using ACL2s in one of the Labs.


Books and Supplies

There is no required book. Instead, we will be using lecture notes. These notes will be posted in intervals before or alongside the lectures. You should read them as soon as they are available: if you read them before the lecture, you may not understand every single item, yet you will be much better prepared for the lecture, and get much more out of it.

Homeworks

There will be approximately 10 homeworks. For most of them you will work in a team of size 2. You are free to choose your own partner (even from the other section), and you can change partner assignment for each homework.

We strongly recommend that you first try to solve the problems on your own. Then meet with your teammate to go over your solutions, resolve disagreements and try to solve any remaining problems.

Frequently asked questions

What if I have questions about the homework?

We will use Piazza for homework clarification questions. Do not email technical questions to the teaching staff.

Obviously, before a homework is due do not post any solutions you have come up with on Piazza. Do not ask "Is this correct?" kind of questions before the due time; they will not be answered. We will help with clarification questions and general advice.

How do I submit my homework?

We will use Blackboard for homework submissions. Do not send homework by email.

Is the due time firm? How do I get an extension?

The due time (usually Saturdays at 5pm) is firm, and there will be no extensions. The submission system will automatically close at the due time. If you cannot finish on time, submit whatever you have; partial credit will be given. Also see Grading below about what if you miss a homework.
Labs

We are running labs in the form of interactive practice sessions. Participation in the labs is voluntary, but if you participate, you have to do so in the lab that was assigned to you.

All labs happen on Fridays, the day before each homework is due (Saturday). So labs are a good opportunity to brush up on lecture material, which may help you solve some remaining homework puzzles. (Remember, however, that you are not allowed to discuss your homework solutions with non-team members prior to submission.)

Labs are mostly run by tutors. The format in which labs are conducted are much within the discretion of the tutor, but typically activities include: the tutor solves a problem at the board with student interaction; a student solves a problem at the board with student interaction; students solve a problem on their own and then discuss their findings; a possible solution is projected to the screen and then critiqued by everyone; etc.


Challenge Problems

These are optional problems that you can try to solve in order to broaden your horizon, and to earn a few extra points. Expect these problems to be "real-life": quite hard, perhaps a little ambiguous, non-straightforward. Points for them are not meant as a give-away. The frequency of challenge problems, and how much each is worth, will be determined as the class goes along.

You must not discuss these problems with anyone outside your group other than the instructor.

Grading

The grading scheme for the class is composed of mandatory points
(homework, quizzes, exams) and experience points. The idea is that mandatory points are given for class components that you are expected to participate in, while experience points are "extra credit". To get the best possible grade in this class, it is sufficient to obtain all of the mandatory points.

A. Mandatory points: Here is the percentage of each component's contribution to the mandatory part of your grade. Note that, as per the above rule, these percentages add up to 100.

Midterms: there will be two, on the following days:

Here and here are two (first) midterm exams from a previous semester, given at around the same time in class. We will not provide solutions to these earlier exams. Here are some review problems for the second midterm.

The midterms will take place for both sections at 6pm in 101 Churchill Hall, i.e. not during regular class hours. Each midterm will last approximately 65mins. You must be present at the midterms, since makeup exams will generally not be given. Therefore, mark those days in your calendars.

Final: there will be one, on the following day:

The final exam will be comprehensive. Again, you must be present, since makeup exams will generally not be given.

Here is the Final exam from Spring last year.

All exams are pencil-and-paper and closed-book; no electronics will be allowed. However, you may take one double-sided sheet of paper to each exam, with whatever contents you like, hand-written or printed, in whatever font size you like.

Homeworks: will be assigned almost every week; exceptions are exam weeks, and Spring break. There will be about 10 in total. For each homework we will grade only a subset of the problems. At the end of the semester, we will drop the lowest homework grade.

Quizzes: will be given approximately once a week, and graded. If you are not present for a quiz, you will get zero points, with no make-ups. On the other hand, at the end of the semester we will drop the two lowest quiz grades.

B. Experience points:
These are extra points awarded for substantial additional efforts like solving challenge problems that will be offered in class (and possibly for minor efforts like finding critical errors in the lecture notes). Again, these are extra points that you don't need to pursue, but you can use them to compensate for a lack of points in mandatory components. Solving challenge problems will also expand your horizon beyond the class material. These problems will be hard: don't rely on them as a cheap way of filling point gaps elsewhere.
The following table shows the percentages of the total course points that guarantee a particular letter grade.

A
A-
B+
B
B-
C+
C
C-
D+
D
D-
F
93
90
87
83
80
77 73
70
67
63
60
<60

As required by the registrar, at the end of the semester you will get two grades for this course: one for the lecture, and one for the lab. The rules are:

Points for homeworks, quizzes and exams will be entered on Blackboard. You are strongly encouraged to check that we enter the right points for you. If you notice any data entry errors, please inform us right away. You have one week after the cause for your disagreement has emerged.


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.

An example of an Academic Integrity violation that we have had problems with in the past and will therefore monitor carefully is:

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.