Tik-79.146 Logic in Computer Science: Special Topics I

Spring 1999

(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, proof theory and computational properties) 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)
Modal Logic V
Translation to predicate logic, multi-modal logic, decidability and computational complexity
tutorial 8 (solutions)
Modal Logic VI
Introduction to temporal logic; CTL and LTL
tutorial 9 (solutions)
tutorial 10 (solutions)
Modal Logic VII
CTL vs. LTL; Expressing properties of systems; model checking
Modal Logic VIII
Tableau method for CTL
tutorial 11 (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 Tuesday 16.2.99 at the lecture 16-18 o'clock.
    The deadline for the first assignment is Tuesday 9.3.99.

  2. The second home assignment is distributed starting on Tuesday 30.3.99 at the lecture 16-18 o'clock. The deadline for the second assignment is Tuesday 20.4.99.

  3. The third home assignment is distributed starting on Tuesday 27.4.99 at the lecture 16-18 o'clock. The deadline is Tuesday 11.5.99. 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 TB336.

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

If you have returned your assignment, see the results (situation on 5.10.99).


Other Interesting Stuff

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

Maintained by Ilkka.Niemela@hut.fi