Syllabus
CS 2800 is a 4-credit course.
Course Description
Introduces the connections of basic mathematical logic to computing. 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 undergraduate advising office and the instructor.
Class Times and Location
Mon, Wed, Thu, 9:15--10:20am, West Village 110
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 Communication below), office hours, email (last resort). Try these options in this order until you succeed.
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 installing and using ACL2s in one of the Labs.
Books and Supplies
There is no required book. The following book is recommended:
Logic in Computer Science, by Michael Huth and Mark Ryan.
Cambridge University Press, ISBN: 978-0-521-54310-1
(2nd edition, paperback).
The book is not required since we cover only a fairly small amount of material from the book. Relevant pointers will be provided.
In addition, we will be using lecture notes ("Notes"). The Notes are somewhat raw: less formal than the recommended textbook, but closer in contents to what we do in class, so it is strongly recommended that you follow these Notes.
In fact, read the Notes as soon as they are posted (new posts will be announced), even when the topic has not yet been covered in the lectures: this will optimally prepare you for the lecture. You do not have to understand everything from the Notes before it is covered.
The textbook and even the Notes go beyond what we cover in the lectures. You will only be examined on material that is covered in the lectures or in the homeworks.
Homeworks
There will be approximately weekly homeworks. For most homeworks you will work in a team of size 2. You are free to choose your own partner, and you can change partner assignment for each homework.Labs
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.
What if I have questions about the homework?
We will use Piazza (see Communication above) 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.
If the homework is to be done in pairs, both partners must submit, the submission for both partners must be the same solution file, and the solution file must contain the names of both partners near the top. This is our way of checking that partnership is by mutual consent.
What is the due date and time? How do I get an extension?
Unless otherwise stated on the homeworks page, homeworks are due Saturdays by 5pm.
Why this crazy time? because it gives you the opportunity to ask the course staff questions about the homework during the Friday Lab on the day before it is due, and also because it gives you a lecture-free day to finish your homework. This due time is not an obligation nor even an invitation for you to do the homework on Saturdays!
The due time 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.
How are homeworks evaluated?
For each homework we will grade only a subset of the problems. At the end of the semester, we will count the nine best of your homework grades.
We are running labs in the form of interactive practice sessions. You have to participate 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 the due time.)
Labs are mostly run by tutors. The format in which labs are conducted are much within the discretion of the tutor, but typical 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.
Labs will be graded. At the end of the semester we will count the ten best of your lab grades.
Exams
We have two midterm exams, one final, and various quizzes. All of these are mandatory.
Midterms: they will be on the following days:
The midterms will take place during regular class hours. Each midterm will thus last 65mins. You must be present at the midterms, since makeup exams will generally not be given. Therefore, mark those days in your calendars.
- Thursday, Sep 25 2014
- Thursday, Oct 23 2014
Final:
- day to be determined by the registrar
The final exam will be comprehensive. Again, you must be present, since makeup exams will generally not be given.
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.
Here are some exams from previous years. They are posted by popular request; do not rely on the exams this semester being "very similar".
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. At the end of the semester we will count the ten best of your quiz grades.
Course grade
Here are the contributions of various course components to your grade. These percentages add up to 100.
The following table shows the percentages of the total course points that guarantee a particular letter grade. These percentages may be relaxed down, up to the discretion of the instructor.
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:
- you will receive the same letter grade X in the lecture and in the lab, and
- grade X will be entirely determined by your performance in the lecture part of the course.
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; 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.