Logic and Computation
CS 2800 Summer2018

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

Lectures: M-Th 1:30-3:10pm BK 320

Labs: T / Th 3:20-5pm WVH 210

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

You are required to check for announcements daily, which will be posted on piazza.

Rules

Books and Supplies

Currently you do not need to purchase anything for the course....unless Poll Anywhere stinks. In that case we'll change systems). 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.

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.

Please read and sign the Course Contract.

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, the course contract and see Mitch Wand's Web page on the topic.

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.

During in class quizzes, looking at how someone else voted without permission will be considered cheating.

We reserve the right to computationally detect cheating. This may be via TurnItIn, MOSS, or any other plagarism detections software.

Exams

There are exactly two exams. They are scheduled for

Grading

Grades will be determined as follows.

There are only 2 exams and there is no final.

Quizzes will occur regularly. Be prepared for a short quiz every day. Quizzes will require the use of a computer or cell phone. Only a subset of the quizzes might be graded. If you are not present for a quiz you will get 0 points. We will drop the lowest 10% of quizzes. Half of your quiz grade will be participation.

Homeworks will be given about twice a week. Your homework grade will be based on your top ten homeworks. You will mostly work in groups of 2 or 3 (max). We recommend that you to first try to solve the problems on your own. Then meet with your partners to go over your solutions and solve any unresolved problems. We may only grade a subset of the problems assigned. Homeworks will be due on Tuesdays and Fridays at 11:59PM (we can change this if it regularly collides with another course.

Labs do not directly contribute to your grade. You will spend most of your time in labs working on problems that we distribute in advance. If you solve the problems on your own before lab and are confident in your solutions, there is no need to show up. If you did not have time to solve the problems, or you tried and ran into trouble, then go to lab. Although labs are "optional" they are highly recommended. If you struggle with the course, my first question tends to be "are you going to labs?"

Grading Notes

Prerequisites

CS 1800 and CS 2500.
If you do not have this background you should get the permission of the instructor. Our policy is that we do not grant exemptions if you did not getting passing grades in both the prerequisites: experience has shown that this is the best policy for students.

Schedule

Week
Topics
May 7
L1-L4
  1. Introductions & motivation
  2. Syllabus, class web page, programming review
  3. Designing data-driven programs, the ACL2s development environment
  4. Basic data types, expressions, syntax & semantics of atomic data and associated primitive functions
  5. Syntax & semantics of lists, design considerations of the ACL2s core language
May 14
L5-L18
  1. Contracts, termination, useful macros, let
  2. Data types: enumerated, range, product, record, union, list, (mutually) recursive
  3. Property-based testing, test?, program mode and defunc settings
  4. Boolean logic, one-time pads
  5. Properties of Boolean operators, characterization of formulas, introduction to P=NP
  6. Proof methods: instantiation, case analysis, equational proofs, truth tables, decision procedures
May 21
L9-L12
  1. Limitations of Boolean logic, intro to equational reasoning for programs
  2. Axioms for equality, cons-first-rest axioms, definitional axioms, instantiation, contract checking and completion
  3. Equational reasoning in the presences of implications, context vs. theorems, undecidability results
  4. Equational reasoning with nested Boolean operators, derived context
  5. Reasoning about arithmetic, program equivalence: proving correctness of an exponential-time improvement, numeric reasoning in C & other languages
  6. The equational reasoning recipe and examples
May 29
L13-L15
  1. Exam Review
  2. Definitions: soundness, termination, contracts, the ACL2s Definitional Principle
  3. Termination, measure functions
  4. Using termination to show soundness of common recursions schemes and the design recipe, the undecidability of termination analysis, big-Oh analysis as a refinement of termination
June 5
L16-L19
  1. Proof by contradiction, mathematical induction, well-foundnesses, a proof that mathematical induction works, how to extract induction schemes from admissible recursive functions
  2. Using induction to prove program correctness
  3. Induction like a professional
  4. Data-function-induction trinity
  5. Generalization, lemma generation, dealing with induction failure
June 12
L20-L23
  1. Intro to reasoning about accumulators
  2. Tail recursion: efficiency considerations, how to prove correctness
  3. Accumulator reasoning examples
  4. Reasoning about algorithms & libraries: sorting, correctness
  5. Designing and reasoning about libraries
  6. Abstract and algebraic data types
  7. Observational equivalence
June 18
L24-L27
  1. Makeup class
  2. Exam2 Review
  3. Reasoning about imperative programs
  4. A look back: Logic and the birth of computer science; A look forward: what's next