CS 245E: Logic and Computation (Enriched) — Fall 2019

Course Outline

This page will be updated from time to time during the term. The original start-of-term version is also available.

Time and Place

Lectures:

TuTh 1:00–2:20, ML 349 OPT 309.

Tutorials:

Fridays, 10:30–11:20, RCH 308.
(Except Nov. 8; the IA will be busy marking midterms.)

Resources

Textbooks (optional)

M. Huth and M. Ryan, Logic in Computer Science (2nd ed.), Cambridge University Press, 2004.
G. Dowek, Proofs and Algorithms: An introduction to logic and computability, Springer, 2011.
These are available for purchase (optional) at the UW store. The Davis Centre library has copies on reserve (electronic for Dowek, bound for Huth/Ryan).

Electronic fora

Piazza: for questions and discussion from students, and announcements, discussion and answers from instructors.
Note that Piazza posts are completely public, and may be read by anyone anywhere.
Learn: for sensitive and/or confidential information.
Assignments and solutions. Record of marks (grade computations may be unreliable).

Other

Additional material (e.g., copies of overheads, etc.) will be posted from time to time.

Personnel

Role Name Email Contact
Instructor Jonathan Buss jfbuss DC 3353, x34428.

Hours: Mon., 1:00–2:00, Wed., 10:00–11:00, or by appointment, or just drop by.

Instr. Asst. and TA Stephanie McIntyre srmcintyre Tutorial Center (MC 4065)
Hours: Mon., 10:00–11:00 11:00–12:00.
TA Jan Gorzny
Yetian Wang
jgorzny
yetian.wang
n/a
ISC Dalibor Dvorski ddvorski MC 4102, x36816

For questions regarding course material and/or logistics, do any/all of

To request a re-evaluation of marking, or to discuss your progress in the course, contact the instructor.

For administrative issues, including illness forms and accommodation for religious holidays, see either the instructor or the ISC.

For other issues, or if nothing applies, please contact the instructor.

Course Work

Grading summary:

Academic Integrity and Students with Disabilities

This courses adheres to the UW policies on Academic Integrity and Students with Disabilities.

Course Topics

(This outline will be annotated with times and readings, as the course progresses.)

Course overview. Readings: H&R, §1.1
  • The place of logic in mathematics, including computer science.
  • Formal vs. informal logic.
Basic (propositional) logic.
Readings: H&R, §§1.1, 1.3, 1.4.1, 1.4.2.
  • The stuff of propositional logic: propositions and truth values.
  • Well-formed formulas. Values of formulas.
  • Properties of formulas and their relationships.
    Reading: Laws of Boolean algebra (updated: 17/9/19).
  • A first formal proof system—Resolution.
    Reading: Propositional Resolution (full version, with minor revisions: 24/9/19).
Predicate logic (first order)
Readings: H&R, §§2.1, 2.2, 2.4.
Optional: Dowek: §§ 1.2.1–2, 1.3, 2.1. (This presentation has greater generality, different notation, and far fewer examples than H&R. Caveat lector.)
Overheads on values of quantified formulæ.
  • The stuff of predicate logic: domains and quantification.
  • Extending propositional syntax and semantics. Examples in math and CS.
  • A look at Resolution for predicate logic.Omitted.
Formal proofs via Natural Deduction
  • Deduction rules for propositional logic and predicate logic. Examples.

    Readings: H&R, §§1.2, 2.3. (Propositional summary: p. 27.)
    Dowek, §1.4. (For a variation, see §1.6.)

  • Properties of deductive systems: soundness, completeness, and compactness.
  • Relation to other formal deductive systems.
Using logic in math/CS
Readings: Notes on Peano Arithmetic and on formal lists (preliminary version)
  • Arithmetic.
    Orderings.
    Lists and other stuctures.
  • Definability. Limits to definability.
Computation
Readings: Dowek, §§3.1, 3.2, 3.4.1. Also see §3.4.2.
Notes on recursive functions.
Notes interpretation of recursive functions, and on the incompleteness of mathematics.
  • Recursive functions. Relations to other computational modes; the Church-Turing Thesis.
  • Non-primitive recursive functions; non-recursive functions.
  • Undecidability in computation and in logic. Gödel's Theorem.
Programming = Proof ?
  • The Curry-Howard Correspondence. Propositions as types.
  • Constructive logic as a foundation for computation.
    Implications for design of programming languages.
  • Computing proofs.

Campaign Waterloo

David R. Cheriton School of Computer Science
University of Waterloo
Waterloo, Ontario, Canada N2L 3G1

Tel: 519-888-4567 x33293
Fax: 519-885-1208

Contact | Feedback: cs-webmaster@cs.uwaterloo.ca | David R. Cheriton School of Computer Science | Faculty of Mathematics


Valid HTML 4.01!Valid CSS! Last modified: Tuesday, 26-Nov-2019 11:12:05 EST


Menu:ShowHide