CS 270 Mathematical Foundations in CS - Syllabus

Term and Credits

Spring 2023-2024
3 Credits

Room and Time

Section Days Time Room Instructor Course Assistant
002 MW 10:30am - 11:50am 3675 Market Street Room 1104 Steve Earth Andy Chek
003 TR 1:30pm - 2:50pm 3675 Market Street Room 1104 Mark Boady Andy Chek
004 TR 3:00am - 4:20am 3675 Market Street Room 1104 Mark Boady Andy Chek

Instructors

Professor Mark Boady
Electronic Mail Address: mwb33@drexel.edu
Office: 3675 Market Street Room 1063 (near snack machine)
Extention: 215-895-2347
Office Hours: Tuesday and Thursday 5-6PM

Professor Steve Earth
Electronic Mail Address: se435@drexel.edu
Office: 3675 Market Street Room 1169
Office Hours: every weekday (except week2) 9:30-10:30am

Teaching Assistant(s)

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

Name Email Hours
Andy Chekacc374@drexel.eduM 12:00PM-2:00PM, W 2:00PM-4:00PM
Tsion Bekeletsb97@drexel.eduT 6:00PM-8:00PM

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

Forall x: Calgary
P.D. Magnus and Tim Button
http://forallx.openlogicproject.org

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 logic and proofs.
Connecting Discrete Mathematics and Computer Science - 2nd Edition
David Liben-Nowell
ISBN-13: 978-1009150491
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.

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,

Course Material

Programming Language

Lectures

Labs

Homeworks

Exams

Extra Credit

General Information

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:

Appropriate Use of Course Materials

It is important to recognize that some or all of the course materials provided to you are the intellectual property of Drexel University, the course instructor, or others. Use of this intellectual property is governed by Drexel University policies, including the IT-1 policy found at: https://drexel.edu/it/about/policies/policies/01-Acceptable-Use/
Briefly, this policy states that all course materials including recordings provided by the given prior written approval by the University. Doing so may be considered a breach of this policy and will be investigated and addressed as possible academic dishonesty, among other potential violations. Improper use of such materials may also constitute a violation of the University's Code of Conduct found at: https://drexel.edu/cpo/policies/cpo-1/ and will be investigated as such.

Recording of Class Activities:

In general, students and others should not record course interactions and course activities in lecture, lab, studio or recitation.
Students who have an approved accommodation from the Office of Disability Resources to record online lectures and discussions for note taking purposes should inform their course instructor(s) of their approved accommodation in advance. The recording of lectures and discussions may only be carried out by the students enrolled in the class who have an approved accommodation from Disability Resources with their instructors' prior knowledge and consent. Students with approved accommodations may be asked to turn off their recorder if confidential or personal information is presented.
If a student has any comments, concerns, or questions about provided class materials and/ or recording, talk to your course instructor first. If this does not resolve the issue, you can also reach out to the Department Head, and use the process described for a grade appeal to move your concern forward. The process described for grade appeals can be found at: https://drexel.edu/provost/policies/grade-appeals/

Tentative Course Schedule

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

NOTE: Due to University Holidays the TR and MW sections have different due dates.

Week Topic Homework
(1) 4/1/2024 Lecture 1: Formal Logic
Lecture 2: Natural Deduction Basics
Lab 1 - Due at end of Lecture 2
(2) 4/8/2024 Lecture 3: Disjunction Elimination
Lecture 4: Proofs by Contradiction
Lab 2 - Due at end of Lecture 3
Lab 3 - Due at end of Lecture 4
Homework 1 - Due 11:59PM Friday (4/12/24)
(3) 4/15/2024 Lecture 5: Predicates and First Order Logic
Lecture 6: Deduction with Predicates
Lab 4 - Due at end of Lecture 5
Lab 5 - Due at end of Lecture 6
Homework 2 - Due 11:59PM Friday (4/19/24)
(4) 4/22/2024 Lecture 7: Introduction to Racket
Lecture 8: Recursion and Lists
Lab 6 - Due at end of Lecture 7
Lab 7 - Due at end of Lecture 8
Homework 3 - Due 11:59PM Friday (4/26/24)
(5) 4/29/24 Lecture 9: Equational Reasoning
Lecture 10: High Order Functions
Lab 8 - Due at end of Lecture 9
Lab 9 - Due at end of Lecture 10
Homework 4 - Due 11:59PM Friday (5/3/24)
(6) 5/6/24 Lecture 11: Inductive Thinking
Midterm
Lab 10 - Due at end of Lecture 11
Midterm - In Class During Second Lecture of Week
(7) 5/13/24 Lecture 12: Mathematical Induction
Lecture 13: Peano Arithmetic
Lab 11 - Due at end of Lecture 12
Lab 12 - Due at end of Lecture 13
Homework 5 - Due 11:59PM Friday (5/17/24)
(8) 5/20/24 Lecture 14: Induction on Lists
Lecture 15: Boolean Expressions as Lists
Lab 13 - Due at end of Lecture 14
Lab 14 - Due at end of Lecture 15
Homework 6 - Due 11:59PM Friday (5/24/24)
(9) 5/27/24 Lecture 16: Boolean Normal Forms
Lecture 17: Simplifying Expressions Recursively
Lab 15 - Due at end of Lecture 16
Lab 16 - Due at end of Lecture 17
Homework 7 - Due 11:59PM Friday (5/31/24)
(10) 6/3/2024 Lecture 18: SAT Solvers
Lecture 19: NP-Complete Problems
Lab 17 - Due at end of Lecture 18
Lab 18 - Due at end of Lecture 19
Homework 8 - Due 11:59PM Friday (6/7/24)
(11) 6/10/24 Final Exam Time/Room June 12, 2024 01:00 pm - 03:00 pm Main/Admin Building AUD
Extra Credit Course Survey - Due 11:59PM Wednesday (6/12/24)