TCS / Studies / T-79.3001 Logic in Computer Science: Foundations
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

T-79.3001

Logic in Computer Science: Foundations

(4 cr)

Spring 2007 (periods III and IV)

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

Previous years: [Spring 2006] [Autumn 2004]

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.


Current


General Information

  • Registration for the course ended on January 22, 2007 at 12:00 hours. Late registration is still possible by contacting the lecturer.
  • Lectures are given by Docent, D.Sc.(Tech.) Tomi Janhunen: Mondays 10—12, hall T1, starting on the 15th of January, 2007
  • Tutorials are held by Lic.Sc.(Tech.) Emilia Oikarinen, M.Sc.(Tech.) Matti Järvisalo, and M.Sc.(Tech.) Antti Hyvärinen:
    • Tuesdays, 16—18, T3, or
    • Wednesdays, 10—12, T2, or
    • Thursdays, 16—18, T2.
    Tutorials start on the 23rd of January, 2007.
  • Course material: lecture notes in Finnish.
  • In order to pass the course one has to
    • pass three compulsory home assignments and
    • pass an exam (with a grade greater than 0).
    The grade may be affected by bonus points (see tutorials and course feedback for details).
  • Brochure in Finnish
  • Office hours: please see the lecturer's home page.
  • Contacts via email: the alias t793001 at tcs.hut.fi is recommended. Please do not forget to mention your student ID!
  • Newsgroup: opinnot.tik.logiikka (using nntp) at news.tky.fi

For Students from Previous Years:

  • The last exam based on course requirements for Spring 2006 is arranged in March 2007.
  • Any unfinished home assignments can be completed by then.
  • Bonus points earned by doing tutorial exercises apply to examinations arranged after March 2007.
Back to menu.

Course Material

Lecture Notes

  • Slides for the lectures to be held in Finnish:
  • Demonstration problems from tutorials (including 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

Lectures are mainly based on two textbooks that we recommend as the main references for foreign students:

Copies of both textbooks are available in the main library as well as the library of CSE department. The material presented at tutorials will be translated into English (which enables English speaking students to attend).

Back to menu.

Lectures

Period III

Propositional Logic

Tentative schedule for lectures:
Lecture 1 (15.1.2007)
Practical arrangements
Brief introduction
Syntax of propositional logic (Section 1)
Lecture 2 (22.1.2007)
Semantics of propositional logic (Sections 2 — 3.5)
Lecture 3 (29.1.2007)
Semantics (continued) and semantic tableaux (Sections 3.6 — 4.3)
Lecture 4 (5.2.2007)
Tableau proofs (continued) and comparison with classical proofs (Sections 4.4 — 5)
Lecture 5 (12.2.2007)
Normal forms and resolution (Sections 6 — 7.3)
No lecture (19.2.2007)
Skiing holidays
Lecture 6 (26.2.2007)
Resolution and computational complexity (Sections 7.4 — 8)

Period IV

Predicate Logic

Lecture 7 (12.3.2007)
Syntax and semantics of predicate logic (Sections 1 — 2.2)
Lecture 8 (19.3.2007)
Semantics (continued) and normal forms (Sections 2.3 — 3)
Lecture 9 (26.3.2007)
Semantic tableaux (Section 4)
Lecture 10 (2.4.2007)
Knowledge presentation (Section 5)
No lecture (9.4.2007)
Easter holidays
Lecture 11 (16.4.2007)
Herbrand's theorem and unification (Sections 6—7)
Lecture 12 (23.4.2007)
Resolution and program verification (Sections 8—9.1)
Lecture 13 (30.4.2007)
Program verification (continued; Sections 9.2—9.5), Summary
Back to menu.

Tutorials

In each two-hour tutorial, there will be three tutorial problems to be solved by students on their own beforehand and two or three demonstration problems. Tutorials are not compulsory but bonus points (from -2 to +3) for exams will be awarded on the basis of them. If you want to solve tutorial problems, please get registered for one of the tutorial groups using TOPI by January 22, 2007 (to enable bookkeeping your tutorial points).

Period III Period IV
T1Week 4 Jan 23—25
T2Week 5 Jan 30—Feb 1
T3Week 6 Feb 6—8
T4Week 7 Feb 13—15
T5Week 8 Feb 20—22
T6Week 11Mar 13—15
T7 Week 12 Mar 20—22
T8 Week 13 Mar 27—29
T9 Week 14/15Apr 3—4, and 12
T10Week 16 Apr 17—19
T11Week 17 Apr 24—26
T12Week 18 May 2—3

Each tutorial problem is worth one tutorial point which implies the maximum of 36 tutorial points. In order to earn one tutorial point, you are supposed solve one problem on your own and to declare it as done at the respective tutorial session. Accordingly, you may be asked to present your solution at the white board. Tutorial points are converted into bonus points using the following scheme:

Tutorial points Bonus points
0—5 -2
6—11 -1
12—17 0
18—23 +1
24—29 +2
30—36 +3

Tutorial Exercises

Tutorial Points

Back to menu.

Home Assignments

  • Each student receives three personal home assignments (HAs) during the spring term.
  • Grading is done using the scale passed / not passed.
  • Please observe: one must pass all the three HAs before attending exams.
  • Assignments will be delivered through our home assignment server.
  • Schedule for spring 2007:

    HA Launch date Deadline
    1 Feb 5, 2007 Feb 15, 2007, 24:00
    2 Mar 28, 2007 Apr 9, 2007, 24:00
    3 Apr 3, 2007 Apr 27, 2007, 24:00

  • If you need help with your home assignments please attend special office hours that are organised on the 17th, 19th, 24th, 26th of April in room TB357 at 15:00—16:00 hours.
  • Results: list of students who have completed all three home assignments (as of Apr 27, 2007, 24:00).
  • New submissions and corrections are still accepted.
Back to menu.

Gaining bonus points from feedback

  • 4 monthly periodic time tracking questionnaires and a general course feedback questionnaire = 2 exam points
  • you get the points only if you fill out all the (five) WWW questionnaires on time!
  • Specifics of time tracking:
    • Links to the questionnaires will be provided when the questionnaires are open (see schedule below)
    • You should keep track on the hours you spend on
      • attending lectures
      • attending tutorials
      • solving the tutorial exercises
      • doing other course-related things (including exam and studying for exam)
    • Time tracking schedule:

      PeriodTracking periodQuestionnaire Open
      1January 15—February 8February 9—16
      2February 9—March 15March 16—23
      3March 16—April 12April 13—20
      4 April 13—May 11 May 11—18

  • Course feedback is collected in the end of the course, give your feedback between April 25th - May 23rd
  • List of students who answered the first time tracking questionnaire on time
  • List of students who answered the second time tracking questionnaire on time
  • List of students who answered the third time tracking questionnaire on time (note: to gain the bonus points you have to answer ALL questionnaires on time!)
Back to menu.

Examinations

Back to menu.
[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 17 March 2008. Tomi Janhunen