|
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
Back to menu.
Lecture Notes
- Slides from the lectures in Finnish:
- 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.
Back to menu.
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.
Back to menu.
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.
Back to menu.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 11 October 2005.
Tomi Janhunen
|