Back
Applied logic (2018/2019)
Lectures take place on odd Wednesday 9:15 - 11:00 in room 21/C-3.
This course is for Master students in Faculty of Electronics.
Materials and literature
- G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual
- M. Ben-Ari, Principles of the Spin Model Checker
- spinroot.com
- M. Ben-Ari, Mathematical Logic for Computer Science
- J. Cichoń, Wykład ze Wstępu do Matematyki (in Polish)
Final mark
There will be homeworks during the semester.
Each solution should be written by hand on a piece of paper (no pdf files!).
Homework 1 (deadline 3.04)
- (2 points) Write a sentence $(p\rightarrow q)\leftrightarrow r$ in CNF and DNF.
- (2 points) Using a resolution method check if $S=\{\overline{p}qr, p\overline{q}r, p\overline{q}\overline{r}, \overline{p}s\}$
is satisfiable. If yes, find a valuation $\pi$ such that $\forall \varphi\in S\; \pi(\varphi)=1$.
Results
Homework 2 (deadline 8.05)
- (2 points) Is it true that $\models_K \Box p\lor\neg\Diamond p$?
- (2 points) Prove that $R$ is a transitive relation on $X$ if and only if $(X,R)\models\Box p\rightarrow\Box\Box p$.
Results
Homework 3 (deadline 05.06)
- (2 points)Is it true that $\models_{LTL}(pUq)\rightarrow (p\lor q)$?
- (2 points) Let $\mathbb{A}=(\{s,t,u\},\Sigma,\{s\},\delta,\{u,t\}),$ where $\Sigma=\{0,1\}$ and $\delta $ is described by the following tabular:
$S$ | $\Sigma$ | $\delta$ |
$s$ | $0$ | $\{t\}$ |
$s$ | $1$ | $\emptyset$ |
$t$ | $0$ | $\{u\}$ |
$t$ | $1$ | $\{u\}$ |
$u$ | $0$ | $\{s,t\}$ |
$u$ | $1$ | $\{s\}$ |
Find $L(\mathbb{A})$ and $L_{\omega}(\mathbb{A})$.
-->
Marks
0-4 | 2.0 |
5 | 3.0 |
6-7 | 3.5 |
8 | 4.0 |
9-10 | 4.5 |
11-12 | 5.0 |
Activity during classes can increase mark up to +1.0.
Final test
The final mark is equal to 40%C+60%T, where C is a mark of classes, T - a mark of final test.
To get a positive mark ($\ge 3.0$) both C and T must be positive.
Schedule
- Propositional logic
- Propositional variables, connectives, sentences, valuations
- Tautologies, satisfiable sentences
- Conjunctive normal form CNF
- Resolvent, resolution method
- Connection to $P=NP$ problem
- Modal logic
- Kripke's frame, Kripke's model
- Language ${\mathcal L}_{ML}(\mathcal P)$, special connectives $\Box, \Diamond$
- Semantics
- Modal tautologies
- Kripke's frames with reflexive, transitive and symetric relation
- Logic $S4,\; S5$
- Theory of a class of Kripke's frames
- Tautologies of $S4$
- Linear Temporal Logic
- Language ${\mathcal L}_{LTL}(\mathcal P)$, new connectives $\bigcirc,\ U$
- Semantics
- Tautologies of $LTL$
- Examples of $LTL$-sentences describing special behaviour of given system
- Wolper's example
- Finite automatons
- Deterministic and nondeterministic finite automatons
- Regular expressions and regular languages
- Buchi automatons
- NBA and DBA
- $\omega$-regular languages
- LTL and Buchi automatons
- Automaton $A_\varphi$ which accepts $mod(\varphi)=\{\pi:\ \pi,0\models\varphi\}$
- Examples
- General construction
- Discrete system of states
- Spin
-->
Back