**Term and Credits**

Spring 2019-2020

3 Credits

**Room and Time**

Section | Days | Room | Instructor |
---|---|---|---|

002 | Tuesday/Thursday | Online Only | Mark Boady |

003 | Tuesday/Thursday | Online Only | Mark Boady |

004 | Tuesday/Thursday | Online Only | Mark Boady |

**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 2-4PM,
Thursday 4-6PM

**Teaching Assistant(s)**

Steve Earth

*Electronic Mail Address:*
se435@drexel.edu

*Office:* Live In Slack Space

*Office Hours:*
Monday 10AM-12PM,
Monday 12PM-2PM,
Tuesday 10AM-12PM,
Tuesday 12PM-2PM,
Thursday 10AM-12PM,
Thursday 2PM-4PM

*CLC Information:*
https://www.cs.drexel.edu/clc

Amira Mefteh

*Electronic Mail Address:*
am3836@drexel.edu

*Office:* Live In Slack Space

*Office Hours:*
Wednesday 10AM-12PM,
Friday 12PM-2PM
*CLC Information:*
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**

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

**Topics**

- Functional Programming
- Recursion, Recursive Definitions and Induction
- Propositional and Predicate Logic
- Formal Proof using Natural Deduction
- Applications of Logic to Computer Science
- Divide and Conquer Algorithms and Recurrence Relations
- Program Specification and Verification
- Automated Reasoning
- Termination Analysis
- 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**

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

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

- Use Proofs by Deduction to Justify Logical Statements
- Be able to write and analyze Recursive Functions
- Be able to implement and use a SAT solver.
- Use Inductive Proofs to Justify the correctness of programs and statements.
- 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

*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**

- Homeworks: 20%
- Labs: 20%
- Quizzes: 10%
- Midterm: 25%
- Final Exam: 25%

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.

- [100-97] A+
- (97-93] A
- (93-90] A-
- (90-87] B+
- (87-83] B
- (83-80] B-
- [80-77] C+
- (77-73] C
- (73-70] C-
- (70-67] D+
- (67-60] D
- (60-0] F

**Late Policy**

- Quizzes
- If you miss a quiz, you must get permission from a TA or Professor to take it late.

- Late Labs/Homeworks
- Penalties:
- -10% 1 day late
- -20% 2 days late
- -30% 3 days late
- -40% 4 days late
- Not Accepted after 4 days

- Penalties:
**Special Exceptions:**In exceptional circumstances, the**Professor**may wave additional penalties or accept work past the cut-off. Please message the Professor directly to request a special exception. Documentation (Doctor Note, Police Report, Athletics Approval, etc) is generally preferred.**Family Friendly Policy:**We understand that some students have family obligations. If you need to miss class for a family emergency please use the Special Exceptions policy. Small children are allowed in class, but please do your best to keep classroom distruptions to a minimum.

**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,

- Failing grade for class
- Deduction of one letter grade
- Zero on Assignment/Exam Violation took place on

**Programming Language**

- This class will use the Racket Programming Language.
- This class will use the DrRacket IDE for developement.
- You may use Racket from the command line instead of the IDE.
- Download Racket

**Lectures**

- Lectures will be recorded and posted at the beginning of each week.
- You may watch the lecture videos at any time.

**Labs**

- You may work in groups of up to 4 students on labs.
- Labs are intended to help you learn the material.
- Collaboration with other students during labs is encouraged.
- Submit lab answers as a word/text/pdf. You do not have to answer on the lab sheet.
- Clearly label each question number.
- Labs are due at 11:59PM
- Labs must be submitted to learning.drexel.edu

**Homeworks**

- Most Weeks will have a homework assignment.
- Homeworks are due at 11:59PM
- Homeworks must be submitted to learning.drexel.edu

**Quizzes/Exams**

- There will be two online exams and 4 quizzes.
- Exams/Quizzes will be open book.
- Exams/Quizzes must be completed individually.

**Slack Channel**

- This term, we will be using a Slack channel instead of a discussion board.
- Our Slack Space is https://join.slack.com/t/cs270spring2020/signup
- You must use an @drexel.edu email to sign up.

**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:

- Academic Honesty: http://www.drexel.edu/provost/policies/academic_dishonesty.asp
- Judicial Affairs Academic Integrity: http://drexel.edu/studentlife/community_standards/facultystaff/integrity/
- Official Final Exam Schedule: http://www.drexel.edu/registrar/scheduling/exams/
- Students with Disability Statement: http://drexel.edu/oed/disabilityResources/overview/
- Course Drop Policy: http://www.drexel.edu/provost/policies/course_drop.asp
- Drexel Student Learning Priorities: http://www.drexel.edu/provost/irae/assessment/outcomes/dslp/
- The instructor may, at his/her/their discretion, change any part of the course during the term, including assignments, grade brakdowns, due-dates, and the schedule. Such changes will be communicated to students via the course web site Announcements page. This page should be checked regularly and frequently for such changes and announcements. Other announcements, although rare, may include class cancellations and other urgent announcements.

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

Week | Topic | Reading | Homework |
---|---|---|---|

(1) April 6, 2020 | 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 |

(2) April 13, 2020 | 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 |

(3) April 20, 2020 | Number Representations |
Peano Axioms
Binary Arithmetic |
Lab 5 and Lab 6 Homework 3 |

(4) April 27, 2020 | Boolean Logic | Chapter 2.1-2.6 from Book fo Proof |
Lab 7 and Lab 8 Homework 4 Quiz 1 Tuesday |

(5) May 4, 2020 | Normal Forms and SAT Solvers |
MiniSat in Browser Boolean Satisfiability Problems |
Lab 9 and Lab 10 Quiz 2 Tuesday |

(6) May 11, 2020 | Natural Deduction |
Deduction Proof Checker Chapter 4 from Book of Proof |
Midterm Tuesday Lab 11 Thursday Homework 5 |

(7) May 18, 2020 | Natural Deduction (continued) |
Chapter 6 from Book of Proof
Pages 142 to 183 of Symbolic Logic: A First Course |
Lab 12 and 13 Homework 6 |

(8) May 25, 2020 | Predicate Logic |
Chapter 2.6-2.12 from Book fo Proof (predicates)
Predicate Logic Slides from CMU |
Lab 14 and Lab 15 Homework 7 Quiz 3 Tuesday |

(9) June 1, 2020 | Proof By Induction |
Chapter 10 from Book of Proof |
Lab 16 and Lab 17 Homework 8 Quiz 4 Tuesday |

(10) June 8, 2020 |
Final Exam - Online Available from 8AM Monday June 8 until 11:59PM Tuesday June 9. Final will be 1 hour and 45 from time started. |