CS 270 Mathematical Foundations in CS - Syllabus

Term and Credits

Fall 2018-2019
3 Credits

Room and Time

Instructors

Professor Jeremy Johnson (Section 1)
Electronic Mail Address: johnsojr@drexel.edu
Office: University Crossings 139
Extention: 215-895.-2893
Office Hours: Wed 10-12PM

Professor Mark Boady (Section 2 and 3)
Electronic Mail Address: mwb33@drexel.edu
Office: University Crossings 138
Extention: 215-895-2347
Office Hours: Wednesday 11am-1pm, Friday 11-1PM, others days/times by appointment.

Teaching Assistant(s)

All TA Office Hours held in the CLC https://www.cs.drexel.edu/clc

Course Description

Introduces formal logic and its connections to Computer Science. Students learn to translate statements about the behavior of computer programs into logical claims and to prove such assertions using both traditional techniques and automated tools. Considers approaches to proving termination, correctness, and safety for programs. Discusses propositional and predicate logic, logical inference, recursion and recursively defined sets, mathematical induction, and structural induction.

Course Objective and Goals

  1. To use recursion and divide and conquer to solve problems
  2. To provide recursive definitions of patterns and data structures
  3. To formally specify the input/output requirements of programs
  4. To use induction and other proof techniques to prove properties of algorithms, data structures, programs, and computer systems
  5. To use logic to describe the state of systems and to use logical deduction (by hand and using tools) to prove properties of systems
  6. To understand the power and limitations of formal logic.

Audience and Purpose within Plan of Study

This is a required course for all Computer Science and Software Engineering students. It should also be of interest to Computer Engineering, Mathematics students and students with an interest in logic and computation.

Prerequisites
Students should have programming experience (CS172 or equivalent).

What Students Should Know Prior to this Course

  1. Ability to read and understand code.
  2. Basic understanding of program execution.
  3. Ability to write simple recursive programs.

What Students will be able to do upon Successfully Completing this Course:

  1. Use Proofs by Deduction to Justify Logical Statements
  2. Be able to write and analyze Recursive Functions
  3. Be able to implement and use a SAT solver.
  4. Use Inductive Proofs to Justify the correctness of programs and statements.
  5. Use logic to describe the state of systems.

Textbook

We will use free resources for this class.

Optional Resources

Book of Proof (Second Edition)
Richard Hammack
Paperback: ISBN 978-0-9894721-0-4
Hardcover: ISBN 978-0-9894721-1-1
Available for Free online at: http://www.people.vcu.edu/~rhammack/BookOfProof/

The Racket Guide
Matthew Flatt, Robert Bruce Findler and PLT
https://docs.racket-lang.org/guide/index.html

Course Material

Programming Language

Lectures

Labs

Quizzes

Homeworks

Exams

Special Circumstances

Course Policies

Academic Honesty Policy

The CCI Academic Honesty policy is in effect for this course. Please see the policy at http://drexel.edu/cci/resources/current-students/undergraduate/policies/cs-academic-integrity/.

Academic Honesty Violations will be reported to the University. Punishment will be determined by the severity of the incident. Punishments include, but are not limited to,

Grading and Policies

Final grades will be determined by your total points weighted according to this distribution. Grades may be curved but are generally computed via the formula below. It may be modified at the instructor's sole discretion, but letter grades will generally not be lower than those shown here.

Computer/Software Help
iCommons: http://drexel.edu/cci/about/our-facilities/rush-building/iCommons/

University Policies
In addition to the course policies listed on this syllabus, course assignments or course website, the following University policies are in effect:

Topics

  1. Functional Programming
  2. Recursion, Recursive Definitions and Induction
  3. Propositional and Predicate Logic
  4. Formal Proof using Natural Deduction
  5. Applications of Logic to Computer Science
  6. Divide and Conquer Algorithms and Recurrence Relations
  7. Program Specification and Verification
  8. Automated Reasoning
  9. Termination Analysis
  10. Test Case and Counter Example Generation

Tentative Course Schedule

Please see the appropriate assignment webpages for a detailed description of course deliverables.

Week Topic Supplemental Links Lab Homework
1 (9/24/18) Introduction to Racket Quick: An Introduction to Racket with Pictures
So You Want to be a Functional Programmer (Part 1)
Lab 1 and Lab 2 Homework 1 - Due 10/4/18 at 11:59PM
2 (10/1/18) List Processing and Natural Numbers List, Iteration, and Recursion
High-order list operations (Ignore Haskell Part) Peano Axioms
Lab 3 and Lab 4 Homework 2 - Due 10/11/18 at 11:59PM
Quiz 1 - Due 10/11/18 at 11:59PM
3 (10/8/18) Boolean Expression and Prepositional Logic
No Classes Monday (Columbus Day)
Chapter 2.1-2.6 from Book fo Proof Lab 5 (Friday class lab 6 also) Homework 3 - Due 10/18/18 at 11:59PM
4 (10/15/18) Predict Logic Chapter 2.7 from Book fo Proof
Predicate Logic
Lab 6 and Lab 7 Homework 4 - Due 10/25/18 at 11:59PM
Quiz 2 - Due 10/25/18 at 11:59PM
5 (10/22/18) Specification and Logic Lab 8 and Lab 9 Online Midterm Due 11/1/18 at 11:59PM
6 (10/29/18) Midterm + SAT Solver MiniSat in Browser
Boolean Satisfiability Problems
Lab 10 and Lab 11 Homework 5 - Due 11/8/18 at 11:59PM
7 (11/5/18) Natural Deduction Chapter 4 from Book of Proof
Deduction Proof Checker
Pages 142 to 164 of Symbolic Logic: A First Course
Lab 12 and Lab 13 Homework 6 - Due 11/15/18 at 11:59PM
Quiz 3 - Due 11/15/18 at 11:59PM
8 (11/12/18) Proofs by Contradiction Chapter 6 from Book of Proof
Deduction Proof Checker
Pages 164 to 183 of Symbolic Logic: A First Course
Lab 14 and Lab 15 Homework 7 - Due 11/29/18 at 11:59PM
9 (11/19/18) Thanksgiving Week - Classes Monday Only
Lab 16 (except WF section)
10 (11/26/18) Mathematical Induction Chapter 10 from Book of Proof
Lab 17 and Lab 18 Homework 8 - Due 12/6/18 at 11:59PM
Quiz 4 - Due 12/6/18 at 11:59PM
11 (12/3/18) Structural Induction   Lab 19 and Lab 20 Homework 9 - Due 12/13/18 at 11:59PM
12 (12/10/18) Final Exam - Time and Location TBD