Term and Credits
Spring 20162017 (April 03, 2017June 16, 2017)
3 Credits
Room and Time
Lectures:
Instructor
Mark Boady
Electronic Mail Address: mwb33@drexel.edu
Office: University Crossings 138
Extention: 2158952347
Office Hours: MWF: 1:00pm2:30pm. By Appointment other Days/Times. (I tend to be around Tuesday.)
Teaching Assistant(s)
Office Hours and Contact Info Through the CLC: https://www.cs.drexel.edu/clc
Grading Details
Your work is graded by multiple people. You should know who to contact for each type of assignment.
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
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).
Textbook
You are required to sign up for an account using the online textbook.
Required Online Text: OLI Logic and Proofs. A code for our class's version of the textbook will be distributed in class. Purchase from http://oli.cmu.edu
Recommended: This book gives a good introduction to Functional Programming in LISP style languages. This is a good additional resources for the programming part of the class. It is not required. Reading will not be assigned from it.
The Little Schemer (4th Edition)
Daniel P. Friedman, Matthias Felleisen
ISBN10: 0262560992
ISBN13: 9780262560993
Available through the
Drexel Bookstore
Also available from 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.
In Class Exercises
Assignments
Additional Policies
Software and Hardware Requirements
All Drexel students are required to have individual access to a dedicated computer which meets minimum specifications, including: processor speed, memory and secondary storage requirements, connectivity via highspeed or direct connection to campus network, and a CD/DVD drive.
Programming assignments will be completed using the Racket Programming Language. It is required for this course. It can be downloaded from https://racketlang.org/
OLI's Proof and Logic programs require Java and Flash. They work best in Firefox.
Academic Honesty Policy
The CCI Academic Honesty policy is in effect for this course. Please see the policy at http://drexel.edu/cci/resources/currentstudents/undergraduate/policies/csacademicintegrity/ .
Computer/Software Help
iCommons: http://drexel.edu/cci/about/ourfacilities/rushbuilding/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.
Week  Topic  Reading  Notes 
1 (4/3/17)  Functional Programming 101 
Required:
Quick: An Introduction to Racket with Pictures
So You Want to be a Functional Programmer (Part 1) Suggested: OLI Chapter 1  Syntax and Symbolization Recursion Explained with the Flood Fill Algorithm (and Zombies and Cats) 

2 (4/10/17)  Introduction to Boolean Logic 
Required: OLI Chapter 2  Semantics Suggested: Chapter 2 Logic from Book of Proof 
HW 1 Due 4/12/17 at 11:59PM 
3 (4/17/17)  Proofs by Deduction  Required: OLI Chapter 3  Derivations  HW 2 Due 4/19/17 at 11:59PM 
4 (4/24/17)  Proofs by Contradiction 
Required: OLI Chapter 4  Indirect Rules Suggested: Chapter 6 Proof by Contradiction from Book of Proof 
HW 3 Due 4/26/17 at 11:59PM 
5 (5/1/17)  Predicate Logic and Metamathematics  Required: OLI Chapter 6  Elementary Metamathematics  HW 4 Due 5/3/17 at 11:59PM 
6 (5/8/17)  Mathematical Induction  Required: Chapter 10 Mathematical Induction from Book of Proof  HW 5 Due 5/10/17 at 11:59PM 
7 (5/15/17)  Proofs on Recursive Data Structures  TBD 
Midterm Due 5/17/17 at 11:59PM Extra Credit 1 Due 5/17/17 at 11:59PM 
8 (5/22/17)  Proving Properties of Recursive Functions  TBD  HW 6 Due 5/24/17 at 11:59PM 
9 (5/29/17)  No Class Monday (Memorial Day) Automated SAT Solvers 
TBD  HW 7 Due 5/31/17 at 11:59PM 
10 (6/5/17)  Termination Proofs Friday: Final Review 
TBD  No In Class Exercise HW 8 Due 6/7/17 at 11:59PM 
11 (6/12/17)  Final Exam  Extra Credit 2 Due 6/14/17 at 11:59PM 