Back

Applied logic (2023/2024)

Lectures take place on Monday 9:15 - 11:00 in room 105 C-5.
This course is for Master students in Control Engineering and Robotics, Faculty of Electronics.

Materials and literature

  1. G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual
  2. M. Ben-Ari, Principles of the Spin Model Checker
  3. spinroot.com
  4. M. Ben-Ari, Mathematical Logic for Computer Science
  5. J. Cichoń, Wykład ze Wstępu do Matematyki (in Polish)
  6. M. Ben-Ari, Mathematical Logic for Computer Science

Homework 1 (deadline 22.04)

  1. (2 points) Write a sentence $ (p\land q)\leftrightarrow s$ in CNF and DNF.
  2. (2 points) Using a resolution method check if $S=\{\overline{p}\overline{q}r, pqr, pq\overline{r}, \overline{p}\overline{s}\}$ is satisfiable. If yes, find a valuation $\pi$ such that $\forall \varphi\in S\; \pi(\varphi)=1$.

Final mark

There will be 3 homeworks during the semester. For each homework you can get 4 points. Each solution should be written by hand on a piece of paper.
Moreover you can get point when you solve exercise in front of the blackboard (during classes).
For final test you can get at most 18 points.
Final marks:
0-11.9 2.0
12-15.9 3.0
16-18.9 3.5
19-22.9 4.0
23-25.9 4.5
26-29.9 5.0
30+ 5.5

Schedule

  1. Propositional calculus
    1. Propositional variables, connectives, sentences, valuations
    2. Tautologies, satisfiable sentences
    3. Conjunctive normal form CNF and disjunctive normal form DNF
    4. SAT problem
    5. Connection to $P=NP$ problem
    6. Resolvent, resolution method
  2. Modal logic
    1. Kripke's frame, Kripke's model
    2. Language ${\mathcal L}_{ML}(\mathcal P)$, special connectives $\Box, \Diamond$
    3. Semantics
    4. Modal tautologies
    5. Kripke's frames with reflexive, transitive and symetric relation
    6. Logic $S4,\; S5$
    7. Theory of a class of Kripke's frames
    8. Tautologies of $S4$
  3. Linear Temporal Logic
    1. Language ${\mathcal L}_{LTL}(\mathcal P)$, new connectives $\bigcirc,\ U$
    2. Semantics
    3. Shift lemma
    4. Tautologies of $LTL$
    5. Examples of $LTL$-sentences describing special behaviour of given system
    6. Wolper's example
  4. Finite automata
    1. Deterministic and nondeterministic finite automaton
    2. Languages accepted by NFA
    3. Languages accepted by NFA and DFA are the same

Back