hledat
Rozdíly
Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.
|
mgr-szz:in-pos:10-pos [2019/06/11 10:18] lachmanfrantisek oprava math |
mgr-szz:in-pos:10-pos [2020/04/12 16:56] |
||
|---|---|---|---|
| Řádek 1: | Řádek 1: | ||
| - | ====== IN-POS 10. Konečné automaty (FA) a logiky nad slovy ====== | ||
| - | ===== Zadání ===== | ||
| - | |||
| - | * Logika 1.řádu (FOL) a monadická logika 2.řádu (MSOL): | ||
| - | * syntax a sémantika FOL a MSOL, | ||
| - | * principy převoditelnosti mezi FA a formulemi MSOL. | ||
| - | * Automaty nad nekonečnými slovy a omega-regulární jazyky. | ||
| - | |||
| - | * IA006 | ||
| - | |||
| - | ===== Vypracování ===== | ||
| - | |||
| - | |||
| - | ==== Logika prvního řádu (FOL) nad slovy ==== | ||
| - | |||
| - | <note tip> | ||
| - | FOL obecně je zpracována v jiné otázce: | ||
| - | http://statnice.dqd.cz/home:inf:ap14 | ||
| - | </note> | ||
| - | |||
| - | === Syntax === | ||
| - | |||
| - | ^ ^ ^ | ||
| - | |<m>x,y,z,...</m>| pozice| | ||
| - | |<m>P_a(x)</m>|unární predikát značící, že na pozici <m>x</m> je písmeno ''a''| | ||
| - | |<m>x < y</m>|pozice <m>x</m> je před <m>y</m>| | ||
| - | |<m>\wedge , ∨ , ¬ </m>|logické spojky| | ||
| - | |<m>\forall x, \exists x</m>|kvantifikace| | ||
| - | | |+ rovnost <m>x=y</m>| | ||
| - | |||
| - | ==== Monadická logika druhého řádu (MSO) nad slovy ==== | ||
| - | |||
| - | === Syntax === | ||
| - | |||
| - | ^ ^ ^ | ||
| - | |<m>x,y,z,...</m>|pozice| | ||
| - | |<m>P_a(x)</m>|unární predikát značící, že na pozici <m>x</m> je písmeno ''a''| | ||
| - | |<m>x < y</m>|pozice <m>x</m> je před <m>y</m>| | ||
| - | |<m>\wedge , ∨ , ¬ </m>|logické spojky| | ||
| - | |<m>\forall x, \exists x</m>|kvantifikace| | ||
| - | |<m>X,Y,Z,...</m>| množiny pozic| | ||
| - | |<m>x \in X</m>| <m>x</m> leží v <m>X</m>| | ||
| - | |<m>\forall X, \exists X</m>| kvantifikace nad množinami pozic| | ||
| - | |||
| - | Proměnné ve formuli mohou být: | ||
| - | * **vázané** pomocí kvantifikátoru | ||
| - | * **volné** (zpravidla píšeme za jméno formule) | ||
| - | |||
| - | |||
| - | <box 90% red|Sentence> | ||
| - | sentence = uzavřená formule = formule bez volných proměnných | ||
| - | </box> | ||
| - | |||
| - | === Jazyky zadané sentencí MSO === | ||
| - | |||
| - | * Sentence MSO <m>\phi</m> = vlastnost slov | ||
| - | * Slovo <math>w \in \Sigma^{\star}</math> vlastnost <math>\phi</math>: | ||
| - | * má: <math>w \vDash \phi</math> | ||
| - | * nemá: <math>w \nvDash \phi</math> | ||
| - | * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \nvDash \phi \rbrace </math> | ||
| - | |||
| - | |||
| - | === Valuace formulí === | ||
| - | |||
| - | Valuace přiřazuje hodnotu volným proměnným. | ||
| - | |||
| - | ==== Vztah FA a formulí MSOL ==== | ||
| - | |||
| - | |||
| - | <box 90% red> | ||
| - | Regulární jazyky = jazyky definovatelné MSO. | ||
| - | </box> | ||
| - | |||
| - | === Převod NFA na formuli MSO === | ||
| - | |||
| - | |||
| - | ==== Automaty nad nekonečnými slovy a omega-regulární jazyky ==== | ||
| - | |||
| - | ===== Zdroje ===== | ||
| - | |||
| - | * [[http://www.fi.muni.cz/usr/kretinsky/MSO_Automaty_slides.pdf|slidy: V. Brožek: Logika a regulární jazyky]] | ||
