Tik-79.146 Logic in Computer Science: Special Topics I

Spring 1998

This is an advanced course on logic and its applications in computer science and engineering. Subjects covered this year are: modal logics (syntax, semantics and proof theory) and applications of temporal logic in concurrent and distributed systems.


Lecture Notes *** Home assignments *** Program *** Other Interesting Stuff

Lecture Notes

(Slides in Finnish; Postscript form)
Introduction
Introduction to the course
Refresher
A refresher on propositional and predicate logic
tutorial 1 (solutions)
Modal Logic I
Introduction to modal logics, syntax, semantics, basic properties
tutorial 2 (solutions)
tutorial 3 (solutions)
tutorial 4 (solutions)
Modal Logic II
Example modal logics
tutorial 5 (solutions)
Modal Logic III
Hilbert style proof theory
tutorial 6 (solutions)
Modal Logic IV
Tableau Method
tutorial 7 (solutions)
tutorial 8 (solutions)
Modal Logic V
Translation to predicate logic, multi-modal logic
tutorial 9 (solutions)
tutorial 10 (solutions)
Modal Logic VI
Decidability and computational complexity
Modal Logic VII
Introduction to temporal logic; CTL and LTL
tutorial 11 (solutions)
Modal Logic VIII
CTL vs. LTL
tutorial 12 (solutions)
CTL Model Checking (by Keijo Heljanko)
Introduction to CTL model checking, a CTL model checking algorithm
Modal Logic IX
Tableau method for CTL
tutorial 13 (solutions)

Home Assignments

There are 3 compulsory home assignments (see
Program). Each student is given a personal assignment.
  1. The first home assignment is distributed starting on Monday 9.2.98 at the lecture 14-16 o'clock.
    The deadline for the first assignment is Monday 2.3.98.

  2. The second home assignment is distributed starting on Monday 23.3.98 at the lecture 14-16 o'clock. The deadline for the second assignment is Wednesday 15.4.98.

  3. The third home assignment is distributed starting on Monday 20.4.98 at the lecture 14-16 o'clock. The deadline is Monday 11.5.98. For more detailed instructions, see how to get started, general information and CTL syntax used by the model checker.
The assignments can be returned at the lectures or tutorials or to the box by the room Y418.

If you cannot come to pick up your assignment at the lectures, please contact the lecturer directly.

Other Interesting Stuff

Robbins Algebras Are Boolean
Information on a proof of a famous mathematical conjecture found by an automated theorem prover.

Maintained by Ilkka.Niemela@hut.fi