T-79.144 Logic in Computer Science: Foundations (2 cr)

Autumn 2003

[General Information] [Lectures] [Home assignments] [Examinations] [TOPI]

Previous years: autumns 2002, 2001, 2000, 1999, 1998, 1997 and 1996.

This is an introductory course on logic and its applications in computer science. Subjects covered: propositional logic, predicate logic, induction principle, model and proof theory, semantic/analytic tableaux, resolution, and some examples of applications.

General Information

• Late registration by contacting the lecturer.
• Lectures by Docent, D.Sc.(Tech.) Tomi Janhunen: Tuesdays 12-14, hall T1.
• Tutorials by Lic.Sc.(Tech.) Toni Jussila, Stud.(Tech.) Matti Järvisalo, Stud.(Tech.) Emilia Oikarinen: Tuesdays, 16-17, hall T2, or Wednesdays, 16-17, hall T2, or Thursdays, 11-12, hall T2, or Fridays, 11-12, hall T3.
• Course material: lecture notes in Finnish.
• In order to pass the course one has to
  • pass the three compulsory home assignments and
  • pass the exam (with a grade greater than 0).
• Brochure (.ps 66kB/ .pdf 53kB) in Finnish and English
• Office hours: please see the lecturer's home page.
• Contacts via email: the alias t79144 at tcs.hut.fi is recommended. Please mention your student ID!
• Newsgroup: opinnot.tik.logiikka

Lecture Notes

• Slides from the lectures in Finnish:
  • Introduction (.pdf) including some prerequisites
  • Part I: Propositional Logic (.pdf), slides 1-157.
  • Part II: Predicate Logic (.pdf), slides 1-187.
• Exercises and some solutions will be also provided.
• Lecture notes can be ordered using TOPI.
• Please avoid unnecessary printing of the material to save printers, paper and thus nature !!!

Further Reading

• A textbook by A. Nerode and R. Shore: Logic for Applications, Springer, 1997, 456 p.
• Chapters I-III are recommended as base material for foreign students.
• The first edition of the book (1993, 365 p.) can also be used (Errata).

Tentative Schedule for Autumn 2003

September 9: Lecture 1

Practical arrangements, introduction
Syntax of propositional logic (slides 2-16)
Tutorial 1 (.ps.gz / .pdf) solutions (.ps.gz / .pdf).

September 16: Lecture 2

Semantics of propositional logic, basic concepts (slides 17-46)
Tutorial 2 (.ps.gz / .pdf) solutions (.ps.gz / .pdf).

September 23: Lecture 3

Basic concepts (continued), semantic tableaux (slides 47-71)
Tutorial 3 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

September 30: Lecture 4

Using semantic tableaux, alternative proof systems (slides 72-108)
Tutorial 4 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

October 7: Lecture 5

Normal forms and resolution (slides 109-133)
Tutorial 5 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

October 14: Lecture 6

Resolution (continued), computational complexity (slides 134-157)
Tutorial 6 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

October 21: Lecture 7

Syntax and semantics of predicate logic (slides 1-31)
Tutorial 7 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

October 28: Lecture 8

Semantics (continued), semantic tableaux (slides 32-59)
Tutorial 8 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

November 4: Lecture 9

Counter models, normal forms, knowledge representation (slides 60-83)
Tutorial 9 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

November 11: Lecture 10

Knowledge representation (continued), Herbrand's theorem (slides 84-118)
Tutorial 10 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

November 18: Lecture 11

Unification, resolution and automated theorem prover OTTER (slides 119-163)
Tutorial 11 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

November 25: Lecture 12

Specifying and verifying programs (slides 164-187)
Tutorial 12 (.ps.gz / .pdf), solutions (.ps.gz / .pdf).

December 2: Lecture 13

Review of Lectures 1-12, preparation for the exam
Tutorial 13: some earlier exercises are handled.

Home Assignments

• Each student receives three personal home assignments during the autumn term.
• Grading is on the scale passed / not passed.
• Observe: one must pass all the three home assignments before attending exams.
• Assignments will be delivered through our home assignment server.
• List of 260 students who have passed their first home assignment.
• List of 215 students who have passed their first two home assignments.
• List of 202 students who have passed their all home assignments.
  
• No updates will be made, i.e. these lists are final.

Schedule

• The first home assignment was launched on October 3, 2003.
  Deadline: October 20, 2003, 24:00
• The second home assignment was launched on November 3, 2003.
  Deadline: November 20, 2003, 24:00
• The third home assignment was launched on November 21, 2003.
  Deadline: December 5, 2003, 24:00
• To get help for the 3rd home assignment please attend one of our special office hours (held by Emilia Oikarinen, room TB360):
  • November 27, 16:00 - 18:00.
  • December 2, 14:00 - 16:00.
  • December 3, 16:00 - 18:00.
  • December 5, 16:00 - 18:00.
  • December 11, 16:15 - 18:00.
  • December 12, 16:00 - 18:00.
  We expect that you make your first electronic submission (or at least a sketch of the definitions by hand) before attending these events. Please consult course material (Sections 5.2 and 8.5 in Part II) to get an idea how definitions are written for predicates in a fairly systematic fashion.

Feedback

We welcome your objective opinion. Please use our feedback form.

Examinations

• One must pass all home assignments before attending exams.
• December 16 (in English), final results (published on Jan 14, 2004)
• February 9 (in English), final results (published on Mar 9, 2004)
• May 5 (in English), final results (published on May 25, 2004)
• August 16 (in English), final results (published on September 3, 2004)
• October 4 (in English), final results (published on November 24, 2004)
• Registration is possible two weeks before the exam but allowed only after passing all the three home assignments.
• Questions will be provided in Finnish and in English.
• A collection of earlier examinations is provided for rehearsal purposes. However, the lecturer wishes to emphasize that similar questions need not appear in the next examination.