TCS /
Studies /
T-79.144 /
2001
T-79.144 Logic in Computer Science: Foundations
Autumn 2001
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]
[Examinations]
[Home assignments]
[Schedule]
[TOPI]
[Autumn 2002]
[Autumn 2000]
- 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
- 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
Back to menu.
- Lecture Notes (opetusmonisteet)
- Slides from the lectures in three packages:
- 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).
Back to menu.
We are looking forward to hear your opinion on this course.
Please use our feedback form.
- 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.
Back to menu.
- 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.
Schedule
- The three home assigments were
launched on October 9, November 7, and November 21, respectively.
- The deadlines speficied for Autumn 2002 apply.
Help for the third home assignment
- 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.
Results
- 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.
Back to menu.
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)
Back to menu.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 11 October 2005.
Tomi Janhunen