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

General Information

• Registration was carried out using [TOPI] and we have accepted 394 registrations (maximum 400).
• Late registration takes place by the approval of the lecturer. Please send your request (and any justification) to the contact email address given below. Requests are processed in connection with the lecturer's office hour.
• Lectures by Tomi Janhunen on Tuesdays, 12-14, hall T1
• Tutorials by a team of assistants, namely
  • M.Sc.(Tech.) Toni Jussila
  • M.A. Misa Keinänen, and
  • Stud.(Tech.) Emilia Oikarinen,
  on
  • Tuesdays, 15-16, hall T2, or
  • Wednesdays, 9-10, hall T2, or
  • Thursdays, 8-9, hall T3, or
  • Fridays, 9-10, hall T2
• Office hours: see the lecturer's home page
• Contacts via email: t79144 at tcs.hut.fi. Please mention your student ID!
• Newsgroup: opinnot.tik.logiikka
• The course consists of
  • lectures and tutorials (2+1 hours a week) held in Finnish
  • three compulsory home assignments
  • examinations (arranged four times a year)
• In order to pass the course one has to pass
  • the three home assignments
  • the exam (with a grade greater than 0)
• Brochure in Finnish and English

Material

• Lecture Notes (opetusmonisteet)
  • Slides from the lectures in three packages:
    • I Propositional Logic (pdf),
    • II Predicate Logic (pdf)
    • III Applications (pdf)
  • Exercises and some solutions (pdf) are also included.
  • The course material is currently under a major revision. Therefore we recommend using only the latest edition for Autumn 2001.
  • 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.
  • The first edition of the book (1993, 365 p.) can also be used (Errata).
• Foreign students: If you don't understand Finnish, our recommendation is that you
  • study Chapters I-III from Nerode and Shore's textbook and
  • do some exercises provided in the book or presented at the tutorials (you could also use exercises from last autumn for which we have translations in English).

Feedback

Examinations

• New policy: you must pass all home assignments before attending exams.
• December 18 (in English), final results (published on Jan 15, 2002)
• January 8, (in English), final results (published on Jan 22, 2002)
• May 13, (in English), final results (published on May 28, 2002)
• September 3, (in English), final results (published on Oct 3, 2002)
• Registration for the exams is compulsory and binding (if you register for an exam, then you must attend it).
  Registration is possible two weeks before each examination.
• 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.

Home Assignments

• Each student receives three personal home assignments during the autumn term.
• Assignments are delivered through our home assignment server.
• Solutions are checked automatically
  • every night 24:00 (the first two home assignments) and on
  • daily 8:00, 16:00 and 20:00 (the third home assignment).
• Grading is on the scale passed / not passed.
• One must pass all the three home assignments before attending exams.
• Those who participated the course last year, but dit not pass all the three home assignments, are supposed to go on correcting their answers and/or doing any undone assignments.

• The three home assigments were launched on October 9, November 7, and November 21, respectively.
• The deadlines speficied for Autumn 2002 apply.

• If the third home assignment turns out to be too difficult for you, you may attend special office hours to get help.
• These events were arranged as follows: November 23 and 27, December 4, 7, 11, 13, and 14, and January 2-4.
• Similar events will be arranged during the spring term:
  • January 28 (Misa Keinänen, 16:00-18:00, TB349)
  • February 18 (Misa Keinänen, 16:00-18:00)
  • March 11 (Misa Keinänen, 16:00-18:00)
  • April 8 (Misa Keinänen, 16:00-18:00)
  • April 29 (Misa Keinänen, 16:00-18:00, TB349)
  • Weekly office hours (Tomi Janhunen)
• We expect that you make your first electronic submission (or at least a sketch of the definitions by hand) before attending these events.

• The list of 375 students who have passed their first home assignment (generated on October 30, 2001, 24:00).
• The list of 346 students who have passed their first two home assignments (generated on November 29, 2001, 24:00).
• The list of 298 students who have passed their all home assignments (generated on August 31, 2002, 24:00).
• The last list gives the final results for Autumn 2001.

Lectures and Tutorials

Tentative schedule for Autumn 2001

September 11: Lecture 1

Registration, Practical Arrangements, Introduction, and Prerequisites (slides in ps and pdf)

September 18: No lecture this week, but tutorials (on prerequisites) are arranged

Tutorial 1 (exercises in ps and pdf)

September 25: Lecture 2

Syntax and semantics of propositional logic (slides 1-27 in Package I)
Tutorial 2 (exercises in ps and pdf)

October 2: Lecture 3

Basic semantical definitions, introduction to semantic tableaux (slides 28-52 in Package I)
Tutorial 3 (exercises in ps and pdf)

October 9: Lecture 4

Semantic tableaux: properties and use (slides 53-72 in Package I)
Tutorial 4 (exercises in ps and pdf)

October 16: Lecture 5

Alternative proof systems (by Hilbert and Suppes), normal forms (slides 73-103 in Package I)
Tutorial 5 (exercises in ps and pdf)

October 23: Lecture 6

Clausal form and resolution (slides 104-129 in Package I)
Tutorial 6 (exercises in ps and pdf)

October 30: Lecture 7

Computational complexity (slides 130-139 in Package I),
Syntax of predicate logic (slides 1-20 in Package II)
Tutorial 7 (exercises in ps and pdf)

November 6: Lecture 8

Semantics of predicate logic, semantic tableaux (slides 21-51 in Package II)
Tutorial 8 (exercises in ps and pdf)

November 13: Lecture 9

Complete systematic tableaux, Hilbert's system, normal forms (slides 52-80 in Package II)
Tutorial 9 (exercises in ps and pdf)

November 20: Lecture 10

Representing knowledge with predicate logic, Herbrand's theorem (slides 81-119 in Package II)
Tutorial 10 (exercises in ps and pdf)

November 27: Lecture 11

Unification, resolution (slides 120-146 in Package II)
Tutorial 11 (exercises in ps and pdf)

December 4: Lecture 12

Some applications: theorem prover OTTER, logic programming, correctness considerations of programs (package III)
Tutorial 12 (exercises in ps and pdf)