Tik79.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.
 Lectures by
Ilkka Niemelä:
Mondays 1416, room U344
 Tutorials by
Patrik Simons:
Tuesdays 1617, room U344
 Course material:
Lecture notes.
Fitting, Basic Modal Logic, Handbook of Logic in
Artificial Intelligence and Logic Programming, Volume 1, Logical
Foundations, 1993.
E.A. Emerson, Automated Temporal Reasoning about Reactive Systems,
Logics for Concurrency, F. Moller and G. Birtwistle (Eds.),
SpringerVerlag, 1996, LNCS 1043, pp. 4199.
Articles.
 In order to pass the course one has to
 pass the home assignments
 pass the exam (with a grade greater than 0)
 Newsgroup: opinnot.tik.logiikka
 Brochure in Finnish
(PostScript),
course information at
TOPI
 Exam: 20.5.1998, 1215, ABKLN

Instructions for the exam.

Exam on 21.5.1997

Exam on 26.9.1997

Exam on 20.5.1998
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, multimodal 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.

The first home assignment is distributed starting on Monday 9.2.98 at the
lecture 1416 o'clock.
The deadline for the first assignment is Monday 2.3.98.
 The second home assignment is distributed starting on Monday
23.3.98 at the lecture 1416 o'clock.
The deadline for the second assignment is Wednesday 15.4.98.
 The third home assignment is distributed starting on Monday
20.4.98 at the lecture 1416 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.

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