CS 80 Syllabus

Catalog Description

Introductory logic (propositional and first-order) with a focus on its applications to the field of Computer Science, stressing three aspects of that relationship: the use of logic in programs (AI, databases), the use of logic to reason about programs (program specification and verification), and the relationship between systems of proof and systems of computation. Particular emphasis is placed on syntactic proof systems and computational aspects of proof search, as well as on the use of first-order logic as a descriptive language. Prerequisites: Computer Science 60 and Mathematics 55. 3 credit hours.

Instructor

Joshua S. Hodas 243 Olin, 621-8650 hodas@cs.hmc.edu http://www.cs.hmc.edu/~hodas For schedule and office hours, see schedule on office door, or check http://www.cs.hmc.edu/~hodas/schedule.html

Course Home Page

Bulkpack

A course bulkpack consisiting of copies of all of the lecture slides will be available shortly from King's Copies (330 Foothill, between Yale and Indian Hill on the south side of the street).

Optional Textbook

This book is out of print. We have negotiated the right to copy the entire text with the publisher for royalties of $6.00 per copy. The book can be purchased at King's Copies. The price should be about $29 per copy (including the royalty payment and tax).

Date / Time / Place

Course Outline

• Introduction
• Mathematical Preliminaries
• Propositional Logic
  • Syntax
  • Semantics
  • Proof Systems (Hilbert, Natural Deduction, Sequent Calculus, Resolution)
  • Decidability and Complexity
  • (ITA) Infinitary Formulas and Compactness
• First-Order Logic
  • Syntax
  • Examples
    • Axiomatization of Mathematical Structures
    • Logic as a Data Base Query Language
    • Logic as a Programming Language
  • Semantics
  • Proof Systems (Hilbert, Natural Deduction, Sequent Calculus)
  • Clausal Form
  • Herbrand Theorem
  • Unification and Resolution
  • SLD-Resolution and Prolog
  • (ITA) SLD-Resolution as Gentzen Proof Search
• (ITA) Applications and Other Logics
  • Hoare Logic / Program Correctness
  • Temporal Logic

Grading

There will be weekly to bi-weekly assignments involving the formalisms we will be studying. Most will be written, though there may be one or more involving the use of an online automated deduction system. The homeworks will count for 40-50% of your grade.

There will be two or three programming projects involving developing a resolutiuon-based theorem prover. The projects will each count for 10% of your grade.

There will be two take-home exams (dates to be determined) each counting for 15%.

Grading will be on a ten point scale. Late submissions will be dropped 1.5 points for every two days late. That is, as soon as an assignment is late it will drop 1.5 points. You then have 48 hours to submit it before it drops another 1.5 points. No assignments will be accepted more than four days late.

In addition, You each begin with a bank of five free delay days that you may use as you see fit to reduce late penalties. Note that these are delay days, not banks of 48 hours. Further, the use of delay days does not affect the overall limit of four days late for submission.

With regard to both pencil-and-paper and computer-based assignments we expect you to hold to the following standard in your work: you are free to discuss a problem with other students, and hash out the general framework of the solution, but the actual work handed in must be your own. You should not share code, or substantial aspects of solutions.