CS 270 Mathematical Foundations in CS - Syllabus

Term and Credits

Fall 2019-2020
3 Credits

Room and Time

Section Days Time Room Instructor
001 Tuesday/Thursday 10:00AM-11:50AM 3675 Market Street Room 1052 Mark Boady
002 Tuesday/Thursday 12:00AM-1:50PM 3675 Market Street Room 1052 Mark Boady
005 Tuesday/Thursday 4:00PM-5:50PM 3675 Market Street Room 1052 Galen Long
006 Tuesday/Thursday 6:00PM-7:50PM 3675 Market Street Room 1056 Galen Long
007 Wednesday/Friday 10:00AM-11:50AM 3675 Market Street Room 1104 Galen Long

Instructors

Professor Mark Boady
Electronic Mail Address: mwb33@drexel.edu
Office: 3675 Market Street Room 1058 (near snack machine)
Extention: 215-895-2347
Office Hours: Tuesday 3-4PM, Wednesay 2-4PM Thursday 3-4PM

Professor Galen Long
Electronic Mail Address: nkl43@drexel.edu
Office: 3675 Market Street Room 1153
Office Hours: Monday 10AM-12PM, Wednesday/Friday 12-1PM

Teaching Assistant(s)

Steve Earth (Lead TA)
Electronic Mail Address: se435@drexel.edu
Office: Drexel CLC 3675 Market St Room 1066
Office Hours: https://www.cs.drexel.edu/clc

Jiho Yoo
Electronic Mail Address: jy434@drexel.edu
Office: Drexel CLC 3675 Market St Room 1066
Office Hours: https://www.cs.drexel.edu/clc

Khanh Tran
Electronic Mail Address: kat372@drexel.edu
Office: Drexel CLC 3675 Market St Room 1066
Office Hours: https://www.cs.drexel.edu/clc

Penghu Chen
Electronic Mail Address: pc634@drexel.edu
Office: Drexel CLC 3675 Market St Room 1066
Office Hours: https://www.cs.drexel.edu/clc

Reza Moradinezhad
Electronic Mail Address: rm976@drexel.edu
Office: Drexel CLC 3675 Market St Room 1066
Office Hours: 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.

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

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

CS 172 Minimum Grade: D or CS 176 Minimum Grade: D or CS 265 Minimum Grade: D or SE 103 Minimum Grade: D or ECEC 301 Minimum Grade: D or ECEC 201 Minimum Grade: D

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.

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

Optional:

If you want to learn more about functional programming.
The Little Schemer - 4th Edition
Daniel P. Friedman and Matthias Felleisen
ISBN-13: 978-0262560993
ISBN-10: 0262560992
Available at: Amazon

If you want to learn more about recursive proofs.
The Little Prover - 1st Edition
Daniel P. Friedman and Carl Eastlund
ISBN-13: 978-0262527958
ISBN-10: 0262527952
Available at: Amazon

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.

Course Material

Programming Language

Late Policy

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,

Lectures

Labs

Homeworks

Exams

Slack Channel

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:

Tentative Course Schedule

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

Special Note: Section 007 is Wed/Friday.
Labs/Lectures/Quizzes listed as Tuesday will be done on Wednesday.
Labs/Lectures/Quizzes listed as Thursday will be done on Friday.
Homework Due Dates are the same for everyone.
Week Topic Reading Homework
(1) September 23, 2019 Introduction to Racket Quick: An Introduction to Racket with Pictures
So You Want to be a Functional Programmer (Part 1)
List, Iteration, and Recursion
Lab 1 and Lab 2
Homework 1 - Due October 3, 2019 at 11:59PM
(2) September 30, 2019 Equational Reasoning and High Order Functions How to Write Proofs: a quick guide
High-order list operations (Ignore Haskell Part)
Anonymous Function Tutorial
Lab 3 and Lab 4
Homework 2 - Due October 10, 2019 at 11:59PM
(3) October 7, 2019 Number Representations Peano Axioms
Binary Arithmetic
Lab 5 and Lab 6
Homework 3 - Due October 17, 2019 at 11:59PM
Quiz 1 Tuesday
(4) October 14, 2019 Boolean Logic Chapter 2.1-2.6 from Book fo Proof Lab 7 and Lab 8
Homework 4 - Due October 24, 2019 at 11:59PM
(5) October 21, 2019 Normal Forms and SAT Solvers MiniSat in Browser
Boolean Satisfiability Problems
Lab 9 and Lab 10
Quiz 2 Tuesday
(6) October 28, 2019 Midterm Tuesday
Natural Deduction (Part 1)
Deduction Proof Checker
Chapter 4 from Book of Proof
Lab 11 Thursday
Homework 5 - Due November 7, 2019 at 11:59PM
(7) November 4, 2019 Natural Deduction (Part 2 and 3) Chapter 6 from Book of Proof
Pages 142 to 183 of Symbolic Logic: A First Course
Lab 12 and 13
Homework 6 - Due November 14, 2019 at 11:59PM
(8) November 11, 2019 Predicate Logic Chapter 2.6-2.12 from Book fo Proof (predicates)
Predicate Logic Slides from CMU
Lab 14 and Lab 15
Homework 7 - Due November 21, 2019 at 11:59PM
Quiz 3 Tuesday
(9) November 18, 2019 Proof By Induction Chapter 10 from Book of Proof
Lab 16 and Lab 17
Homework 8 - Due December 5, 2019 at 11:59PM
(10) November 25, 2019 - Thanksgiving - No Classes
(11) December 2, 2019 Structural Induction   Lab 18 and Lab 19
Quiz 4 Tuesday
(11) December 9, 2019 Final Exam - December 12, 2019 8:00AM-10:00AM in Main Auditorium