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
Topics
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
What Students will be able to do upon Successfully Completing this Course:
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
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,
Programming Language
Lectures
Labs
Homeworks
Quizzes/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:
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. |