Tik-79.146 Logic in Computer Science: Special Topics I
Spring 1999
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.
- The course starts on week 4 and the first
lecture is on Feb 26.
- Lectures by
Doc. Ilkka Niemelä:
Tuesday 16-18, room TB333
- Tutorials by
Patrik Simons:
Wednesdays 15-16, room TB353
- 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.),
Springer-Verlag, 1996, LNCS 1043, pp. 41-99.
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
- Exams:
12.5.1999, 9-12, E
26.5.1999, 12-15, T2
-
Instructions for the exam.
-
Results
of the exam on 12.5.1999
-
Results
of the exam on 26.5.1999
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.
-
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.
- 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.
- 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