**Term and Credits**

Summer 2017-2018

3 Credits

**Room and Time**

Tuesday/Thursday 3:30pm-4:50pm University Crossings Room 149

**Instructor**

Mark Boady

*Electronic Mail Address:*
mwb33@drexel.edu

*Office:* University Crossings 138

*Extention:* 215-895-2347

*Office Hours:*
Monday 4-5PM,
Tuesday 12-1PM,
Thursday 12-1PM

**Teaching Assistant(s)**

Alexander Duff

*Electronic Mail Address:*
amd435@drexel.edu

*Office:* Drexel CLC UC 152

*Office Hours:*Monday 2-4PM, Wednesday 2-4PM

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.

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

- 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

**Programming Language**

- This class will use the Racket Programming Language.
- This class will use the DrRacket IDE for developement.
- Download Racket

**Lectures**

- Lectures will be held twice a week.
- Attendance in lecture is required.
- If you need to miss class, please message the Professor to request an exception.

**Exercises**

- Most Classes will have an in-class exercise.
- Exercise is due by the end of class.
- Some exercises will be require working with a team.
- Some exercises will be completed individually.
- If you need to miss class, please message the Professor to request an exception.

**Homeworks**

- Most Weeks will have a homework assignment.
- Homeworks are due Wednesday at 11:59PM
- Homeworks must be submitted to learning.drexel.edu
**Late Submissions:**- 1 Day Late 10 point deducton (Before Thursday 11:59PM)
- 2 Days Late 20 point deduction (Before Friday 11:59PM)
- 3 Days Late 30 point deduction (Before Saturday 11:59PM)
- 4 or More Days Late - Only Accepted with Instructor Permission

**Exams**

- There will be two written exams given in class
- Midterm during class Thursday of Week 6
- Final Exam during Exam Week (Week 11)

**Slack Channel**

- This term, we will be using a Slack channel instead of a discussion board.
- Our Slack Space is cs270-summer2018.slack.com
- You will receive an invite link in a course announcement. Email the Professor if you need assistance.

**Special Circumstances**

- If you have a documented reason why you cannot submit an assignment by the deadline, a special exception may be made. The Professor may also wave the late submission penalty for documented special exceptions.

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

**Grading and Policies**

- In Class Exercises 25%
- Homeworks 25%
- 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

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

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

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

Week | Topic | Reading | Homework |

1 (6/25/18) | Introduction to Racket |
Quick: An Introduction to Racket with Pictures So You Want to be a Functional Programmer (Part 1) |
Homework 1 - Due 7/4/18 at 11:59PM |

2 (7/2/18) | List Processing |
List, Iteration, and Recursion High-order list operations (Ignore Haskell Part) |
Homework 2 - Due 7/11/18 at 11:59PM |

3 (7/9/18) | Natural Numbers | Peano Axioms | Homework 3 - Due 7/18/18 at 11:59PM |

4 (7/16/18) | Propositional Logic: Boolean Functions and Expressions | Chapter 2 from Book fo Proof | Homework 4 - Due 8/1/18 at 11:59PM |

5 (7/23/18) | SAT Solvers |
MiniSat in Browser Boolean Satisfiability Problems |
HW4 Extended to 8/1/18 at 11:59PM |

6 (7/30/18) |
Tuesday - Midterm Review Thursday - Midterm in Class |
||

7 (8/6/18) | Natural Deduction |
Chapter 4 from Book of Proof Deduction Proof Checker Pages 142 to 164 of Symbolic Logic: A First Course |
Homework 5 - Due 8/15/18 at 11:59PM |

8 (8/13/18) | Proofs by Contradiction |
Chapter 6 from Book of Proof Deduction Proof Checker Pages 164 to 183 of Symbolic Logic: A First Course |
Homework 6 - Due 8/22/18 at 11:59PM |

9 (8/20/18) | Mathematical Induction |
Chapter 10 from Book of Proof |
Homework 7 - Due 8/29/18 at 11:59PM |

10 (8/27/18) | Structural Induction | Homework 8 - Due 9/5/18 at 11:59PM | |

11 (9/3/18) | Final Exam - Time and Location TBD |