CS 80 Syllabus

Catalog Description (HMC)

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.

Instructors

Joshua S. Hodas 243 Olin / B-159 Olin (after Early February), 621-8650 hodas@cs.hmc.edu http://www.cs.hmc.edu/~hodas For general schedule and office hours, see schedule on office door, or check http://www.cs.hmc.edu/~hodas/schedule.html For current schedule of actual appointments this week check http://calendar.yahoo.com/jshodas?v=1

Course Home Page

Course Materials

A course bulkpack consisiting of copies of most of the lecture slides will be made available shortly for sale through the CS Department office. Handouts of other slides and notes will occur intermittently in class.

All materials will be made available in PDF form on the course homepage. However, if you expect to want to have the slides on paper, you are encouraged under the honor code, to purchase the bulkpack rather than printing them at college expense.

Optional Textbook

Date / Time / Place

Section 2: Monday, Wednesday 11:00am-12:15pm, in Galileo Pryne.

Section 1: Monday, Wednesday 1:15pm-2:30pm, in Galileo Pryne.

Course Outline

• Introduction
• Mathematical Preliminaries
• Propositional Logic
  • Syntax
  • Semantics
  • Proof Systems (Natural Deduction, Sequent Calculus, Resolution)
  • Decidability and Complexity
  • Applications/Examples
• First-Order Logic
  • Syntax
  • Examples
    • Axiomatization of Mathematical Structures
    • Logic as a Data Base Query Language
  • Semantics
  • Proof Systems (Natural Deduction, Sequent Calculus)
  • Normal Forms, Herbrand Theorem, Unification, and Resolution
• Applications and Other Logics (As Time Allows)
  • Hoare Logic / Program Correctness
  • Temporal Logic

Grading

There will be weekly to bi-weekly written assignments involving the systems we are studying. These homeworks will count for 35% of your grade.

There will be occasional reading assignments covering applications of logic in computer science. You will be required to write short (1-2 page) abstracts of these readings. These abstracts will count for 5% of your grade.

There will be two programming projects involving developing a propositional resolutiuon-based theorem prover, and one project involving using a state-of-the-art first-order theorem prover. The projects will each count for 10% of your grade (30% total).

There will be two take-home exams, one at roughly mid-semester, the other at the end of the term. (Precise dates to be determined.) Each exam will account for 15% of your grade (30% total).

Grading of assignments, projects, and exams will be on a ten point scale. Late assignment and project 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.

You begin the term with a bank of five "delay days" that are used to offset late submissions. (Note, these are delay days, not two-day periods.) All homeworks/projects will be returned with grades calculated from the full 10 points (this way the graders do not need to deal with the late and delay days). At the end of the term we will allocate your delay days optimally to minimize your overall penalty, and then deduct points for the remaining late days according to the above formula.

Note: the avalability of delay days does not affect the overall limit of four days late for any submission.

No late exams ore reading abstracts will be accepted.

This course is run in accordance with the new CS Department Honesty Policy.

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 allowed (even encouraged!) 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 take or share code, or substantial details of solutions.

Suspected cases of plagiarism will be dealt with according to the policies of the student's home school.