# CS 245: Logic and Computation, Winter 2016

David R. Cheriton School of Computer Science

Contents: General Info, Time and Place, Personnel, Announcements, Course Work, Assignments, Resources, Lectures, Tutorials, University Policies

Piazza for announcements and questions.

Learn for marks and assignment solutions.

## General Information

• Course Description: Propositional and predicate logic. Soundness and completeness and their implications. Unprovability of formulae in certain systems. Undecidability of problems in computation, including the halting problem. Reasoning about programs. Correctness proofs for both recursive and iterative program constructions.
• Objectives: At the end of the course, students should be able to
• Formalize English sentences into properly formed formulae in the propositional and predicate logics and to interpret such formulae in English
• Prove the correctness (or incorrectness) of simple formulae in the propositional and predicate logic by natural deduction (or by counterexample) and find errors in purported proofs
• Describe transformational (algebraic) proof for proving statements in the propositional and predicate logic
• Explain the concepts of partial decidability and of undecidability giving examples of each; apply reductions to demonstrate certain problems have these difficulties
• Annotate short programs with loop or recursive invariants to aid in debugging and proving assertions about simple programs
• Prove the correctness of simple programs in a functional language and in a basic subset of an imperative language
• Handbook Description: CS 245 plays a key role in the development of mathematical skills required in the Computer Science program, and thus complements MATH 135 (Algebra), MATH 239 (Graph Theory and Enumeration), and STAT 230 (Probability). The course covers a variety of topics related to "logic and computation" that are required as background for other courses in Computer Science. It differs both in tone and content from a "logic" course one would typically find in a mathematics program. The course aims to:
• Develop discrete mathematics skills
• Improve knowledge of propositional and predicate logic, including key notions, such as the distinction between syntax and semantics and between "provable" and "valid"
• Explore the limits of computers, including computability and non-computabilty
• Use logical skills to reason about computer programs

## Time and Place

Lectures:

• Section 1. 10:00-11:20 T Th MC 1056
• Section 2. 11:30-12:50 T Th MC 1056
Tutorials:
• 1. 8:30-9:20 F MC 4041
• 2. 3:30-4:20 F MC 4040
• 3. 4:30-5:20 F MC 4060
General Office Hours (changes for specific weeks will be posted on Piazza):
• Mon 1:00 - 2:00, Rafael Velazco, in the Consulting Centre, MC 4065
• Mon 3:00 - 4:00, Michael Cormier, in the Consulting Centre, MC 4065
• Tue 2:00 - 3:00, Lila Kari, DC 3132
• Thu 2:00 - 3:00, Lila Kari, DC 3132
• Fri 1:00 - 2:00, Rafael Velazco, in the Consulting Centre, MC 4065

## Personnel

Instructor: Lila Kari , DC3132, x 33336, lila "at" uwaterloo.ca

Support Coordinator: Ahmed Hajyasien, ahajyasien

The Support Coordinator handles much of the administrative paperwork for all sections. See the Support Coordinator regarding

• Requests for re-marking of assignments and exams
• Verification of illness forms
• Requests for exemptions or re-scheduling due to religious holidays
Do not submit requests for changes of section to the Support Coordinator (nor to an instructor). If Quest does not allow you to make a change yourself, contact a CS advisor.

Instructional Assistants: (lead tutorials and hold tutor office hours in the Consulting Centre)

• Michael Cormier, m4cormie
• Rafael Olaechea Velazco, reolaech

## Announcements

Please see Piazza for questions and announcements.

## Course Work

Credit:
• 8 written assignments, 20%. We will count the best 7 out of 8.
• midterm, 35%
• final exam, 45%
• passing the final exam is necessary for passing the course

Midterm: The midterm will be Thursday, February 25, 4:30-6:20pm, Rooms DWE 1501/2527/3522/3522A. The midterm will cover all the material up to reading week. You will be given the handouts on propositional calculus laws (logical equivalences) and natural deduction.

Exam: Final exam, April 12. The exam covers the whole course.

## Assignments

The work you hand in must be your own. Acknowledge any sources you have used. You may discuss the assignment questions verbally with others, but you should come away from these discussions with no written or electronic records. Write your solutions in your own words, from your own head.

Assignments are due Tuesdays, at 10:00 am, in the drop box near MC 4065. No late assignments are allowed, but note that you can skip one assignment without penalty since we only count the best 8 of 9.

Pick-up times for assignments will be announced on Piazza. Solutions will be posted on LEARN.

 # Released Due 1 [pdf] Mon. Jan.11 Tue. Jan. 19, 10:00am 2 [pdf] Mon. Jan.18 Tue. Jan. 26, 10:00am 3 [pdf] Mon. Jan. 25 Tue. Feb.2 , 10:00am For Q2, use truth tables and DNFs to find the logical formula for each output 4 [pdf] Mon. Feb. 1 Tue. Feb.9, 10:00am 5 [pdf] Mon. Feb. 8 Tue. Feb. 23, 10:00am Please note change in variable order in Q2(c), to C, A, B, D 6 [pdf] Mon. Mar. 07 Tue. March 15, 10:00am 7 [pdf] Mon. Mar.14 Tue. Mar. 22, 10:00am 8 [pdf] Tue. Mar. 21, 10:00am Thu. Mar 31, 10:00am Note the 2-day due date extension

## Resources

Books:
• text: [H&R] M. Huth and M. Ryan, Logic in computer science: modelling and reasoning about systems, 2nd ed., Cambridge University Press, 2004.
QA76.9.L63 H88 2004. On-reserve in the DC library.
• [Niss] Nimal Nissanke, Introductory Logic and Sets for Computer Scientists, Addison Wesley, 1999.
QA76.9.L63 N57 1999. This is more elementary.
• Lu Zhongwan, Mathematical Logic for Computer Science, 2nd ed., World Scientific, 1998.
QA76.9.M35 L8 1998. This is for a 4th year course, quite concise and mathematical.
Handouts:

## Lectures

Here is a list of the topics covered in each lecture, with the corresponding text book sections, and the lecture notes from class.

 L01 Tu Jan  6 Notes Introduction. [H&R] 1.1 L02 Th Jan  8 Notes, page 1-20 Truth tables, well-formed formulas. [H&R] 1.1 Exercises L03 Tu Jan  12 Notes, page 21-37 Propositional calculus, syntax [H&R], 1.3, 1.4.2 Notes, pages 1-11 Propositional calculus, semantics [H&R] 1.4.1 L04 Th Jan  14 Notes, pages 12-37 Proving argument validity [H&R] 1.5.1 Notes, pages 1-17 Propositional calculus, laws, normal forms [H&R] 1.5.1, part of 1.5.2 L05 Tu Jan  19 Notes, pages 18-26 Disjunctive normal form, conjunctive normal form [H&R] 1.5.2 Notes, pages 1-21 Adequate set of connectives L06 Thu Jan  21 Notes, pages 22-56 Logic gates, circuits, analysis and simplificaton of code L07 Tue Jan  26 Notes, pages 1-29 Formal (natural) deduction [H&R] 1.2 (with different notation) Exercises L08 Thu Jan  28 Notes, pages 30-48 Formal (natural) deduction - soundness and completeness [H&R] 1.2 (with different notation) L09 Tue Feb.  2 Notes, pages 49-54 Soundness and completeness [H&R] 1.2 (with different notation) Notes, pages 1-31 Resolution for propositional calculus L10 Thu Feb.  4 Notes, pages 32-37 Davis Putnam Procedure, DPP, Soundness and completeness DPP Exercise L11 Tue Feb.  9 Notes Logic and DNA Computing Notes Solving SAT problems with DNA L12 Thu Feb.  11 Notes Predicate calculus: introduction [H&R] 2.1 L13 Tue Feb.  23 Notes Predicate calculus: Syntax [H&R] 2.2 Notes, pages 1-35 Predicate calculus: Semantics [H&R] 2.4 (with different notation) L14 Thu. Feb.  25 Midterm Q&A L15 Tue Mar.  1 Notes, pages 36-52 Predicate calculus: Semantics, interpretations, satisfiability, universal validity [H&R] 2.4 (with different notation) Notes Predicate calculus: Logical consequence, proving validity [H&R] 2.4, part of 2.5 (with different notation) L16 Thu Mar.  3 Notes Formal (natural) deduction in predicate calculus [H&R] 2.3 (with different notation) L17 Tue Mar.  8 Notes, pages 1-30 Resolution in predicate calculus L18 Thu Mar.  10 Notes, pages 31-51 Resolution theorem proving, Soundness of formal deduction L19 Tue Mar.  15 Notes, pages 52-66 Godel's completeness theorem for predicate logic Notes, pages 1-16 Introduction to undecidability [H&R] 2.5 L20 Thu  Mar.  17 Notes, pages 17-67 The Halting Problem and other undecidable problems [H&R] 2.5 L20 Thu  Mar.  17 Notes, pages 17-67 The Halting Problem and other undecidable problems [H&R] 2.5 L21 Tue  Mar.   22 Notes, pages 1 - 20 Peano Arithmetic L22 Thu  Mar.   24 Notes, pages 20 - 33 Peano Arithmetic, Godel's Incompleteness Theorem Notes, pages 1 - 18 Program verification [H&R], Chapter 4 L23 Thu  Mar.   31 Notes, pages 19 - 88 Program verification [H&R] Chapter 4

## Tutorials

Here is some tutorial material (no guarantee this is precisely what's covered).

-->
 T01 Fri Jan  8 Notes T02 Fri Jan  15 Notes T03 Fri Jan  22 Notes T04 Fri Jan  29 Notes T05 Fri Feb.  5 Notes T06 Fri Feb  12 Revised. T07 Fri March  4 Notes T08 Fri Mar  11 Notes T09 Fri Mar  18 Notes T10 Fri Mar  25 Exercises Erratum: In Problem 1, line 9 of the proof, the justification should be (3, 8, = -) T11 Mon Apr.  4 Notes Exercises of the type 6 - 8 (while loops) are only for your information and will not be included on the final exam.

## University Policies (University required text)

This course adheres to the UW Senate's statement of academic integrity, specifically:

In order to maintain a culture of academic integrity, members of the University of Waterloo community are expected to promote honesty, trust, fairness, respect and responsibility. All members of the UW community are expected to hold to the highest standard of academic integrity in their studies, teaching, and research.

The Office of Academic Integrity's website contains detailed information on UW policy for students and faculty. This site explains why academic integrity is important and how students can avoid academic misconduct. It also identifies resources available on campus for students and faculty to help achieve academic integrity in—and out of—the classroom.

### Grievance

A student who believes that a decision affecting some aspect of his/her university life has been unfair or unreasonable may have grounds for initiating a grievance. Read Policy 70-Student Petitions and Grievances, Section 4.

### Discipline

A student is expected to know what constitutes academic integrity, to avoid committing academic offenses, and to take responsibility for his/her actions. A student who is unsure whether an action constitutes an offense, or who needs help in learning how to avoid offenses (e.g., plagiarism, cheating) or about rules for group work/collaboration should seek guidance from the course professor, academic advisor, or the Undergraduate Associate Dean. When misconduct has been found to have occurred, disciplinary penalties will be imposed under Policy 71—Student Discipline. For information on categories of offenses and types of penalties, students should refer to Policy 71—Student Discipline.