During the semester we had lectures and exercises. The lecture schedule is given below. On the exercises we solving tasks from three lists.

Grade from class basis on homeworks. Activity on exercises raised the grade from homework by +1.0.

The final mark is equal to 40%C+60%T, where C is a mark of classes, T - a mark of final test.

On test

1. Resolution
2. Modal tautologies
3. LTL-tautologies
4. Buchi automaton
5. (optional) Buchi automaton + LTL

Schedule:

1. Propositional logic
   1. Propositional variables, connectives, sentences, valuations
   2. Tautologies, satisfiable sentences
   3. Conjunctive normal form CNF
   4. Resolvent, resolution method
2. Modal logic
   1. Kripke's frame, Kripke's model
   2. Language LML(P), special connectives □, ◊
   3. Semantics
   4. Modal tautologies
   5. Kripke's frames with reflexive, transitive and symetric relation
3. Linear Temporal Logic
   1. Language LLTL(P), new connectives ◯, U
   2. Semantics
   3. Tautologies of LTL
   4. Examples of *LTL-*sentences describing special behaviour of given system
4. Finite automatons
   1. Deterministic and nondeterministic finite automatons
   2. Regular expressions and regular languages
5. Buchi automatons
   1. NBA and DBA
   2. ω-regular languages