Autumn 2004

[General Information] [Course Material] [Lectures and Tutorials] [Home Assignments] [Course Feedback] [Examinations] [TOPI]

Previous years: autumns 2003, 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 is only possible by contacting the lecturer.
• Lectures by Docent, D.Sc.(Tech.) Tomi Janhunen: Tuesdays 12-14, hall T1.
• Tutorials by Lic.Sc.(Tech.) Toni Jussila and M.Sc.(Tech.) Emilia Oikarinen:
  • Tuesdays, 16-17, (T.J.), or
  • Tuesdays, 17-18, (T.J.), or
  • Thursdays, 11-12, (E.O.), or
  • Fridays, 9-10, (E.O.).
  • All tutorials are arranged in lecture hall T2.
• 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 (.pdf) 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

Course Material

Lecture Notes

• Slides from the lectures held in Finnish:
  • Introduction (.pdf) includes some prerequisites
  • Part I: propositional logic (.pdf)
  • Part II: predicate logic (.pdf)
• 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 !!!

English Track

• A. Nerode and R. Shore: Logic for Applications, Springer, 1997.

  Chapters I-III: Propositional Logic, Predicate Logic, PROLOG

• M. Huth and M. Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2000.

  Chapter 4: Program Verification

A copy of the first textbook is already available in the CS library and a copy of the second one has been ordered on the 13th of September.

In year 2000, some exercises were translated into English. Although this material is slightly outdated, it may be useful for English speaking students.

Lectures and Tutorials

Tentative Schedule for Autumn 2004

September 14: Lecture 1

Practical arrangements (.pdf), introduction (.pdf)
Syntax of propositional logic (slides 1-16)
September 14-17: Tutorial 1 (.pdf), solutions (.pdf)

September 21: Lecture 2

Semantics of propositional logic, basic concepts (slides 18-47)
September 21-24: Tutorial 2 (.pdf), solutions (.pdf)

September 23 (exceptionally Thursday, 16:15-18:00, hall T1): Lecture 3

Basic concepts (continued), semantic tableaux (slides 48-72)
September 28 - October 1: Tutorial 3 (.pdf), solutions (.pdf)

October 5: Lecture 4

Using semantic tableaux, alternative proof systems (slides 73-103)
October 5-8: Tutorial 4 (.pdf), solutions (.pdf)

October 12: Lecture 5

Comparison of proof systems, normal forms and resolution (slides 104-134)
October 12-15: Tutorial 5 (.pdf), solutions (.pdf)

October 19: Lecture 6

Resolution (continued), computational complexity (slides 135-160)
October 19-22: Tutorial 6 (.pdf), solutions (.pdf)

October 26: Lecture 7

Syntax and semantics of predicate logic (slides 1-27)
October 26-29: Tutorial 7 (.pdf), solutions (.pdf)

November 2: Lecture 8

Semantics (continued) and normal forms (slides 28-51)
November 2-5: Tutorial 8 (.pdf), solutions (.pdf)

November 9: Lecture 9

Semantic tableaux (slides 52-80)
November 9-12: Tutorial 9 (.pdf), solutions (.pdf)

November 16: Lecture 10

Knowledge representation (slides 81-110)
November 16-19: Tutorial 10 (.pdf), solutions (.pdf)

November 23: Lecture 11

Herbrand's theorem, unification and resolution (slides 111-151)
November 23-26: Tutorial 11 (.pdf), solutions (.pdf)

November 30: Lecture 12

Specifying and verifying programs (slides 152-176)
November 30 - December 3: Tutorial 12 (.pdf), solutions (.pdf)

December 7: Lecture 13

Review of course contents (only in Finnish), preparation for the exam
December 7: Tutorial 13: a rehearsal exam (in English)

Home Assignments

• Each student receives three personal home assignments (HAs) during the autumn term.
• Grading is on the scale passed / not passed.
• Observe: one must pass all the three HAs before attending exams.
• Assignments will be delivered through our home assignment server.

Special Arrangements for Autumn 2005

• New submissions and revisions of old ones are still accepted.
• We will organize special sessions to help students having disfficulties with home assignments.
• The goal is to complete HAs by the last exam arranged under the course code T-79.144 in March 2006.
• Please get registered to one of these special sessions using the TOPI system (by the 7th of October, 2005, 14:00 hours). Remember to use the code T-79.144, then select the season "Spring 2005 - Period 2005/06 III" and see the other events defined therein.
• The schedule for these events (still subject to change) is shown below:
• An advertisement published in the newsgroup.

Results for Autumn 2004

• Final list of 161 students who have passed their all HAs (as of September 30, 2005, 24:00). The accounts of these students have now been closed.
• A bonus was granted to students who did their all in time (no longer applicable).
• Lists of students who did their first, second, third HA in time.
• List of stundets who were granted the bonus (no longer applicable).

Course Feedback

We welcome feedback which is collected centrally in Finnish, Swedish, or English.

• To obtain a bonus you are supposed to fill in the form by December 22, 2004 (24:00 hours).
• List of stundets who were granted the bonus (no longer applicable).

Examinations

• One must pass all home assignments before attending exams.
• Summary of bonus points earned for the exams arranged in December and February.
• December 17, 2004 (in English), final results (published Jan 19, 2005)
• February 7, 2005 (in English), final results (published Mar 11, 2005)
• May 11, 2005 (in English), final results (published Jun 7, 2005)
• August 15, 2005 (in English), final results (published Sep 13, 2005)
• October 25, 2005 (in English), final results (published Nov 7, 2005)
• January 10, 2006 (in English), final results (published Jan 17, 2006)
• March 6, 2006 (in English), final results (published Mar 24, 2006)
• No further exams will be arranged under code T-79.144 which is now replaced by T-79.3001.