Logic and Computation
CS 2800 Spring 2010

College of Computer and Information Science
Northeastern University
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.

Textbooks

There is no required textbook. I will be providing lecture notes. There is however an optional book that students may find useful. The book is written for upper level undergraduate students, but it is the best reference for ACL2 currently available.

Tentative Syllabus

Here is an overview of the material that we expect to cover.
  1. Introduction to the ACL2 programming language and review of 211
  2. Propositional Logic
  3. The Basic ACL2 Logic
  4. Effective Use of the ACL2 Theorem Prover
  5. Applications