---
tags: Specializace
---
# ML 2. Výpočetní logika

*Složitost a vyčíslitelnost problému splnitelnosti. Rezoluční metoda ve výrokové a predikátové logice. Jazyk Prolog, relační algebra a Datalog. Tablové důkazy ve výrokové, predikátové a modální logice. Přirozená dedukce. Induktivní inference ve výrokové a predikátové logice. Bisimulace a temporální logiky. (IA008)*

- Zdroje
- <https://is.muni.cz/auth/el/fi/podzim2020/IA008/um/>
- <https://www.fi.muni.cz/usr/kucera/teaching/logic/log.pdf>
- <https://www.fi.muni.cz/~popel/lectures/bak_logika/>
- <http://www.cs.ubbcluj.ro/~gabis/ml/ML-books/McGrawHill%20-%20Machine%20Learning%20-Tom%20Mitchell.pdf>
- A modern approach to AI
- [Popelova stránka na computational logic](https://www.fi.muni.cz/~popel/lectures/complog/index2015.html) - je tam skoro všechno! :wink:

:::danger
**TODO**
- Revize jestli nic nechybí, případně přeformátovat
:::

## Výroková logika

### Syntax

- Tvořena abecedou výrokové logiky:
- Znaky pro výrokové proměnné $A, B, C, ...,$ kterých je spočetně mnoho;
- logické spojky $\wedge, \vee, \neg, \to, \leftrightarrow$
- závorky $($ a $)$
- Formule výrokové logiky je slovo nad abecedou výrokové logiky:
- každý znak pro výrokovou proměnnou je (atomická) formule
- je-li slovo $\varphi$ formule, pak i $\neg \varphi$ je formule
- jsou-li slova $\varphi_1, \varphi_2$ formule, pak také
$(\varphi_1 \circ \varphi_2)$ je formule, kde $\circ \in \{\wedge, \vee,
\to, \leftrightarrow\}$

### Sémantika

- Mějme zobrazení pravdivostního ohodnocení (valuaci) $v$, které každé výrokové
proměnné přiřadí hodnotu 0 nebo 1
$$v: Variables \to \{0, 1\}$$
- Valuaci lze dále induktivně rozšířit na všechny výrokové formule:
$$
\begin{aligned}
v(\neg\varphi) &= \begin{cases}
0 &\text{jestliže } v(\varphi) = 1 \\
1 &\text{jinak }
\end{cases} \\
v(\varphi_1 \wedge \varphi_2) &= \begin{cases}
0 &\text{jestliže } v(\varphi_1) = 0 \text{ nebo } v(\varphi_2) = 0 \\
1 &\text{jinak }
\end{cases}\\
v(\varphi_1 \vee \varphi_2) &= \begin{cases}
0 &\text{jestliže } v(\varphi_1) = 0 \text{ a současně } v(\varphi_2) = 0 \\
1 &\text{jinak }
\end{cases}\\
v(\varphi_1 \to \varphi_2) &= \begin{cases}
0 &\text{jestliže } v(\varphi_1) = 1 \text{ a současně } v(\varphi_2) = 0 \\
1 &\text{jinak }
\end{cases}\\
v(\varphi_1 \leftrightarrow \varphi_2) &= \begin{cases}
0 &\text{jestliže } v(\varphi_1) = 0 \text{ a současně } v(\varphi_2) = 0 \text{ nebo } \\& v(\varphi_1) = 1 \text{ a současně } v(\varphi_2) = 1 \\
1 &\text{jinak }
\end{cases}
\end{aligned}
$$

### Terminologie

- Výroková formule $\varphi$ je
- **pravdivá** (resp. nepravdivá) při valuaci $v$, pokud $v(\varphi) = 1$ (resp.
$v(\varphi) = 0$);
- **splnitelná**, jestliže existuje valuace $v$ taková, že $v(\varphi) = 1$;
- **tautologie**, jestliže $v(\varphi) = 1$ platí pro každou valuaci $v$.
- Soubor $T$ výrokových formulí je splnitelný, jestliže existuje valuace $v$
taková, že $v(\varphi) = 1$ pro každé $\varphi \in T$.
- Formule $\varphi$ je **logickým důsledkem** souboru formulí $T$, psáno
$T \vDash \varphi$, jestliže $v(\varphi) = 1$ pro každou valuaci $v$ takovou,
že $v(\psi) = 1$ pro každou formuli $\psi$ ze souboru $T$.
- 

- Formule $\varphi$ a $\psi$ jsou **ekvivalentní**, psáno $\varphi \approx \psi$
nebo $\varphi \equiv \psi$, pokud pro každé $v$ platí $v(\varphi)=v(\psi)$.
Nebo taky pokud právě $\varphi \vDash \psi$ a $\psi \vDash \varphi$.

### Ekvivalentní úpravy

#### De Morganovy zákony

- $\neg(\varphi \wedge \psi) \equiv \neg\varphi \vee \neg\psi$
- $\neg(\varphi \vee \psi) \equiv \neg\varphi \wedge \neg\psi$

#### Distributivní zákon

- $\varphi \wedge (\psi \vee \xi) \equiv (\varphi \wedge \psi) \vee (\varphi
\wedge \xi$)
- $\varphi \vee (\psi \wedge \xi) \equiv (\varphi \vee \psi) \wedge (\varphi
\vee \xi$)

### Normální formy

- **Literál** je formule $A$ nebo $\neg A$, kde $A$ je výroková proměnná.
- **Klauzule** je formule tvaru $l_1 \vee ... \vee l_n$, kde $n \geq 1$ a $l_i$ je
literál.
- **Duální klauzule** je formule tvaru $l_1 \wedge ... \wedge l_n$, kde $n \geq 1$ a
$l_i$ je literál.
- Formule v **konjuktivní normální formě (CNF)** je formule tvaru $C_1 \wedge ...
\wedge C_m$, kde $m \geq 1$ a každé $C_i$ je klauzule.
- Formule v **disjunktivní normální formě (DNF)** je formule tvaru $C_1 \vee ...
\vee C_m$, kde $m \geq 1$ a každé $C_i$ je duální klauzule.

## Složitost a vyčíslitelnost problému splnitelnosti

### $\text{P}$ a $\text{NP}$ problémy

- $\text{P}$ problémy lze rozhodnout nějakým deterministickým turingovým strojem TM v
polynomiálním čase.
- $\text{NP}$ problémy lze rozhodnout nějakým nedeterministickým TM v
polynomiálním čase.
- "Řešení" problému lze deterministickým TM v polynomiálním čase:
- nalézt, pokud je problém v $\text{P}$;
- ověřit, pokud je problém v $\text{NP}$ (když nám řešení někdo dodá).
- Alternativní definice $\text{NP}$: problém je $\text{NP}$ $\leftrightarrow$ existuje
pro něj polynomiální verifikátor (tj. lze řešení ověřit v polynomiálním
čase).

Pro připomenutí


### Problém splnitelnosti $\text{SAT}$

- $\text{SAT}$ je problém rozhodnout, zda je daná výroková
formule splnitelná tj. zdali existuje nějáká valuace, pro kterou je formule
pravdivá.
- $\text{SAT}$ je $\text{NP}$-úplný (**Cookova-Levinova věta**)
- Důkaz
- Pro dokázání NP-úplnosti, stačí ukázat, že je v NP a že se na něj dá redukovat libovolný NP problém
- Problém $\text{SAT}$ je $\text{NP}$.
- poskytnuté řešení (tj. valuaci), lze deterministicky ověřit v polynomiálním čase vyhodnocením formule
- Libovolný problém $A \in \text{NP}$ lze redukovat na $SAT$:
- Hlavní myšlenka důkazu je, že uvažujeme nedeterministický TM
rozhodující problém $A$ v polynomiálním čase, jehož vstupní slovo $w$
zakódujeme do formule $\varphi$. Daný TM pak $w$ akceptuje iff $\varphi$
je splnitelné.
- Konstrukce formule jde udělat v polynomiálním čase. Její délka je
taktéž polynomiální vzhledem k délce $w$.
- viz
- [Wiki](https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem#Proof)
- [Harvard](http://people.seas.harvard.edu/~cs125/fall14/lec15.pdf)
- [Video od Strejdy](https://is.muni.cz/auth/el/fi/podzim2020/IB107/um/9.3-NP.m4v)

#### Problém splnitelnosti vo výrokovej logike
- DPLL algoritmus pre CNF-SAT: $O(2^n)$ time complexity

#### Problém splnitelnosti v predikátové logice

- je nerozhodnutelný


## Predikátová logika

### Syntax

- Tvořena **jazykem**. Jazyk je systém **predikátových** a **funkčních symbolů**, kde
u každého symbolu je dána jeho **četnost (arita)**. Pokud jazyk neobsahuje
rovnost pak musí obsahovat alespoň jeden predikátový symbol.
- Abeceda predikátové logiky je tvořena:
- Znaky pro proměnné $x, y, z, ...$
- Predikátové a funkční symboly
- Např. $P, R,...$ a $f, g, ...$
- Funkce vrací $hodnotu$, predikát vrací výroky (jen $True/False$ ?)
- Znaky pro logické spojky $\wedge, \vee, \neg, \to, \leftrightarrow$
- Znaky pro kvantifikátory:
- Univerzální $\forall$
- Existenční $\exists$
- Čárka $,$ a závorky $($ a $)$
- Pokud je jazyk s rovností, pak obsahuje symbol $=$

#### Termy

- **Term** jazyka $\mathcal{L}$ je slovo $t$ nad abecedou jazyka $\mathcal{L}$.
Slovo $t$ má jeden z následujících tvarů:
- proměnná;
- $f(t_1, ..., t_n)$, kde $f$ je funkční symbol a $n$ je arita $f$.
- Term je uzavřený, jestliže neobsahuje proměnné.
- Funkční symboly arity 0 jsou konstanty a píšeme je bez závorek.

#### Formule

- **Formule** jazyka $\mathcal{L}$ je slovo $\varphi$ nad abecedou jazyka
$\mathcal{L}$ následujícího tvaru:
- $P(t_1, ..., t_n)$, kde $P$ je predikátový symbol arity $n$ a
$t_1, ..., t_n$ jsou termy
- $t_1 = t_2$, kde $t_1, t_2$ jsou termy
- $\neg\psi$, kde $\psi$ je formule
- $(\psi_1 \circ \psi_2)$, kde $\psi_1, \psi_2$ jsou formule a
$\circ \in \{\wedge, \vee, \to, \leftrightarrow\}$
- $\forall x \psi$, kde $x$ je proměnná a $\psi$ je formule
- $\exists x \psi$, kde $x$ je proměnná a $\psi$ je formule
- **Volný výskyt proměnné** (ukážeme na příkladu):
- Volné výskyty jsou vyznačeny červeně
- $\forall x P(x, \color{red}{y}) \vee \forall y P(\color{red}{x}, y)$
- $\forall x (P(x, \color{red}{y}) \vee \forall y P(x, y))$
- Proměnná je **volná** (resp. vázaná), má-li ve formuli volný (resp. vázaný) výskyt.
- Formule je **uzavřená** (také sentence), jestliže v ní žádná proměnná nemá volný
výskyt.

#### Substituce

- Term $t$ je **substituovatelný** za proměnnou $x$ ve formuli $\varphi$, jestliže
žádný výskyt proměnné v termu $t$ se nestane vázaným po provedení substituce
termu $t$ za každý volný výskyt proměnné $x$ ve formuli $\varphi$.
- $\varphi(x/t)$ značí substituci $t$ za $x$ v $\varphi$. Alternativně značíme
$\varphi[x \mapsto t$].
- Příklady:
- Ve formuli $\exists z:x + y = z$ můžeme za $x$ substituovat term $y + 3$.
- Ve formuli $\exists z:x + y = z$ nemůžeme za $x$ substituovat term $y + z$,
protože proměnná $z$ se stane vázanou proměnnou.
- Pokud na problematické substituci trváme, musíme přejmenovat vázané proměnné:
- např. $\exists z(x=z+z)[x \mapsto z]$ ~> $\exists u (z=u+u)$

#### Unifikace

- Pokud na termy $t_1$ a $t_2$ aplikujeme substituce tak, aby $t_1 = t_2$,
hovoříme o **unifikaci**.
- Příklady:
- $t_1 = f(x, g(x))$ a $t_2 = f(c, x)$ můžeme unifikovat následujícím
způsobem:
- $t_1[x \mapsto c]$ a $t_2[x\mapsto g(c)]$, vyjde nám $t_1 = f(c, g(c))$ a
$t_2 = f(c, g(c))$, tedy $t_1 = t_2$
- $t_1 = f(x, g(x))$ a $t_2 = f(x, y)$
- Můžeme unifikovat dvěma způsoby:
- $t_2[y \mapsto g(x)]$ nebo
- $t_1[x \mapsto g(x), t_2[x \mapsto g(x), y \mapsto g(g(x))]$
- (správně bychom měli nejdříve substituovat u obou termů $x \mapsto x$)
- $t_1 = f(x)$ a $t_2 = g(x)$ nelze unifikovat

### Sémantika

#### Realizace

- Realizace $\mathcal{M}$ jazyka $\mathcal{L}$ je zadána:
- neprázdným souborem $M$, které nazýváme **univerzem** (případně **nosičem**).
Prvky univerza nazýváme **individui**.
- přiřazením, které každému $n$-árnímu predikátovému symbolu $P$ přiřadí
$n$-ární **relaci** $P_\mathcal{M}$ na $M$;
- přiřazením, které každému $m$-árnímu funkčnímu symbolu přiřadí **funkci**
$f_\mathcal{M}: M^m \to M$.
- **Ohodnocení** je zobrazení přiřazující proměnným prvky univerza $M$.
- **Realizace termu** $t$ při ohodnocení $e$ v realizaci $\mathcal{M}$, psáno
$t^{\mathcal{M}}[e]$ (případně jen $t[e]$, je-li je $\mathcal{M}$ jasné z
kontextu), definujeme induktivně takto:
- $x[e] = e(x)$
- $f(t_1, ..., t_m)[e] = f_{\mathcal{M}}(t_1[e], ..., t_m[e])$
- Nyní definujme sémantiku formulí:
- Říkáme, že formule $\varphi$ je pravdivá v $\mathcal{M}$ při ohodnocení $e$,
jestliže $\mathcal{M}\vDash \varphi[e]$.
- Jesliže $\mathcal{M}\vDash \varphi[e]$ pro každé $e$, pak $\varphi$ je
pravdivé v $\mathcal{M}$, psáno $\mathcal{M} \vDash \varphi$.
- $\mathcal{M} \vDash \varphi[e]$ definujeme induktivně:
- $\mathcal{M} \vDash P(t_1, ..., t_m)[e]$ právě když
$(t_1[e], ..., t_m[e]) \in P_\mathcal{M}$
- $\mathcal{M} \vDash \neg\psi[e]$ právě když neplatí
$\mathcal{M} \vDash \psi[e]$
- $\mathcal{M} \vDash (t_1 = t_2)[e]$ právě když $t_1[e]$ a $t_2[e]$ jsou
stejná individua
- $\mathcal{M} \vDash (\psi \to \xi)[e]$ právě když
$\mathcal{M} \vDash \xi[e]$ nebo neplatí $\mathcal{M} \vDash \psi[e]$
- (analogicky pro ostatní spojky)
- $\mathcal{M} \vDash \forall x \psi[e]$ právě když
$\mathcal{M} \vDash \psi[e(x/a)]$ pro každý prvek univerza M
- $[e(x/a)]$ je funkce, která pro $x$ vrací $a$ a pro ostatní argumenty
stejnou hodnotu jako $e$
- Sémantiku formule s existenčním kvantifikátorem máme již definovanou,
protože platí:
- $\exists x \varphi$ je ekvivalentní s $\neg\forall x \neg \varphi$
- Příklad:
- Nechť univerzum jsou všechna přirozená čísla,
- jazyk $\mathcal{L}$ obsahuje unární
predikátový symbol $S$ a binární funkční symbol $+$.
- Realizace $\mathcal{M}$:
- $S$ bude realizován jako sudá čísla tzn. $S_\mathcal{M} = \{2, 4, 6, ...\}$
- $+$ bude realizován jako sčítání čísel (ve formuli použijeme infixový
zápis).
- Příklady formulí:
- Neplatí $\forall x: S(x)$, protože např. $1 \notin S_\mathcal{M}$.
- Platí $\forall x, y: (S(x) \wedge S(y)) \to S(x + y)$, protože součet
dvou sudých čísel je opět sudý.

### Normální formy

#### Prenexová normální forma (PNF)

- Formule je v PNF, právě když jsou **všechny kvantifikátory na začátku formule**.
Za kvantifikátory následuje **"jádro" v CNF nebo DNF**.
- Pro každou formuli existuje ekvivalentní formule v konjuktivní (a taky disjunktivní)
PNF.
- Příklad: $\forall x \forall y \exists z \forall w ((P(x, y) ∨ ¬Q(z)) ∧
(R(x, w) ∨ R(y, w)))$
- 
- 

#### Skolemova normální forma (SNF)

- SNF je **prenexová normální forma pouze s univerzálními kvantifikátory**.
- Idea převodu: nahradíme proměnné, které se vážou na existenční kvantifikátor
- Skolemizací dostaneme formuli, která **zachovává splnitelnost**, tzn. je splnitelná právě tehdy, když originální formule byla splnitelná
Skolemovými funkcemi:
- Převedeme $\forall x_1...\forall x_n \color{red}{\exists y}
P(x_1,..., x_n, \color{red}{y})$ na
$\forall x_1...\forall x_n P(x_1,..., x_n, \color{red}{f(x_1, ..., x_n)})$.
- 

## Rezoluční metoda ve výrokové a predikátové logice

- Rezoluce je metoda založená na **vyvrácení** (dokazuje se nesplnitelnost formulí).
- Je vhodná pro strojové dokazování (např. Prolog).

### Rezoluce ve výrokové logice

- Budeme pracovat s klauzulemi:
- Literál je formule $A$ nebo $\neg A$, kde $A$ je výroková proměnná.
- Klauzule je formule tvaru $l_1 \vee ... \vee l_n$, kde $n \geq 1$ a $l_i$
je literál.
- Píšeme $\{l_1, ..., l_n\}$
- Množinu klauzulí budeme chápat jako jejich konjunkci (tedy CNF)
- Příklad: $\{\{\neg B\}, \{\neg A, B\}, \{A, B, C\}\}$ je
$\neg B \wedge (\neg A \vee B) \wedge (A \vee B \vee C)$
- Rezoluční pravidlo:
- Mějme dvě klauzule $\{L, A_0, ..., A_m\}$ a $\{\neg L, B_0, ..., B_m\}$.
Jejich rezolventou je $\{A_0, ..., A_m, B_0, ..., B_n\}$.
- Rezoluční důkaz:
- Vstup: množina klauzulí $\phi$
- Výstup: `true` pokud je $\phi$ splnitelné, jinak `false`.
- Snažíme se pomocí postupného aplikování rezolučního pravidla získat
prázdnou rezolventu ($\{\emptyset\}$). Pokud takovou množinu najdeme, pak původní
množina klauzulí není splnitelná.
- Rezoluce je pro výrokovou logiku **korektní** a **úplná**.
- Příklad
- 
- Davis-Putnam algoritmus
- 
- tl;dr
- Vyber si proměnnou
- Udělej všechny možné rezolventy s klauzulemi obsahující zvolenou proměnnou
- Odstraň všechny "dostupné" klauzule obsahující zvolenou proměnnou a
klauzule, které jsou tautologie (např. $\{C, \neg C\}$)
- Opakuj
- Příklad
- 
- Bacha na notaci! $\{\} \neq \{\emptyset\} = \{\{\}\}$. V
předešlém příkladu jsme dostali prázdnou rezolventu, takže $\phi = \{\emptyset\}$
a ne $\phi = \emptyset$.

#### Zjemnění rezoluce

- Jde o snahu zmenšit/omezit prohledávaný prostor

##### Lineární rezoluce

- V každém rezolučním kroku použijeme rezolventu z předešlého kroku.
- Lineární rezoluce je **korektní a úplná**.
- 

##### Hornovy klauzule

- Hornova klauzule je kaluzule s nejvýše jedním pozitivním literálem.
- Příklad: $\{A, \neg B, \neg C\}$
- Množina Hornových klauzulí je nesplnitelná iff umíme pomocí lineární rezoluce
odvodit $\emptyset$.

##### SLD rezoluce

- Je lineární rezoluce, kde klauzule jsou posloupnosti a ne množiny. Rezolvujeme
vždy nejlevější literál aktuální klauzule.
- SLD rezoluce je **korektní a úplná pro Hornovy klauzule**.
- Příklad
- 

#### Rezoluce v predikátové logice

- Pracujeme s formulemi v SNF, kvantifikátory nepíšeme.
- Příklad formule: $∀x∀y((P(x, f(x)) ∨ ¬Q(y)) ∧ (¬R(f(x)) ∨ ¬Q(y)))$ reprezentujeme
jako $\{\{P(x, f(x)), ¬Q(y)\}, \{¬R(f(x)), ¬Q(y)\}\}$
- Mezi stejně pojmenovanými proměnnými v různých klauzulích není žádná vazba,
potřebujeme je unifikovat.
- Příklad
- 
- Rezoluce v predikátové logice (bez rovnosti) je **korektní a úplná**.

## Jazyk Prolog

### Syntax

- Datové objekty:
- **termy** jsou konstanty, proměnné nebo složené termy
- konstanty:
- celá čísla `0`, `123`, `-12`
- desetinná čísla `1.0`, `4.5E7`, `-0.12e+8`
- atomy jsou general-purpose jména `'John Doe'`, `s1`
- proměnné:
- řetězec začínající velkým písmenem `X`, `Hodnota`
- složené termy:
- `funktor(term_1, ..., term_n)`
- Příklad: `point(X, Y, Z)` nebo `mother_child(eva, ivana)`
- Prologovský program obsahuje množinu fakt a pravidel.
- Pravidla:
- Tvar `Head :- Body.`
- Příklad:
- `sibling(X, Y) :- parent_child(Z, X), parent_child(Z, Y).`
- `X, Y` jsou proměnné
- Fakta:
- Pouze klauzule bez těla
- Příklad:
- `father_child(lubomir, ales).`
- Dotazy/cíle, na které se ptáme:
- `?- sibling(lubomir, ales).` - jsou lubomir a ales sourozenci?
- `?- sibling(lubomir, X).` - najde všechny sourozence lubomira
- Celkově by mohl program vypadat takto:

  mother_child(trude, sally).
 
  father_child(tom, sally).
  father_child(tom, erica).
  father_child(mike, tom).
  
  sibling(X, Y)      :- parent_child(Z, X), parent_child(Z, Y).
  
  parent_child(X, Y) :- father_child(X, Y).
  parent_child(X, Y) :- mother_child(X, Y).

- A dotaz by se vyhodnotil takto:

  ?- sibling(sally, erica).
  Yes

### Sémantika

- `u :- p, q, ..., t.` odpovídá v logice následující formuli
$u ← p \wedge q \wedge ... \wedge t$, která odpovídá
$u \vee \neg p \vee \neg q \vee ... \vee \neg t$, což je Hornova klauzule.
- Dotaz se vyhodnocuje tak, že se dotaz zneguje a dokazuje sporem pomocí
SLD rezoluce.
- Příklad SLD-stromu
- 
- Příklad jak vypadá přímo SLD rezoluce pro dva dotazy
- 
- Prologovský program **není korektní ani úplný**.
- Prologovský interpretr používá jednodušší a nekorektní způsob unifikace, který ignoruje více výskytů jedné proměnné.
- Unifikuje $p(x, f(x))$ na $p(f(y), f(y))$ (tedy $x \mapsto f(y)$ pro
první $x$ a $x \mapsto y$ pro druhé $x$).
- Úplný není protože se může prologovský program zacyklit (např. špatné
pořadí pravidel).
- Příklad:

#### Řezy

- Při SLD rezoluci dochází k backtrackingu. Ten můžeme kontrolovat pomocí řezů.
Ten uděláme pomocí `!`.
- Příklad:

  a(X, Y) :- b(X), !, c(Y).
  b(1).
  b(2).
  b(3).

  c(1).
  c(2).
  c(3).

Dotaz `?- a(Q, R)` nám vrátí:

  Q=1
  R=1;
  Q=1
  R=2;
  Q=1
  R=3;
  No

Jak vidíme, `Q` se unifikovalo pouze s prvním faktem `q(1).` a neuvažovalo
další možnosti.
- S řezy se musí pracovat opatrně, protože si můžeme "odstřihnout" správnou
větev.

### Příklady kódů, rekurze a seznamy

- [Prolog Tutorial](https://www.javatpoint.com/prolog)
- [Jak funguje append a rekurze](http://cs.union.edu/~striegnk/learn-prolog-now/html/node47.html)
- [Faktoriál](http://rosettacode.org/wiki/Factorial#Prolog)

## Relační algebra

- viz [PB154](https://is.muni.cz/auth/el/fi/podzim2020/PB154/um/03-ch6-formal-query-languages.pdf) a [Kapitola 3: Relační model](https://www.fi.muni.cz/~xdohnal/lectures/PB154/czech/zezula03.pdf)
- Procedurální dotazovací jazyk (kterým uživatel žádá informace z databáze).
- Databáze je množina relací (tabulek).
- Příklad
| flight | from | to | price |
| ------ | :----: | ---------: | ----: |
| LH8302 | Prague | Frankfurt | 240 |
| OA1472 | Vienna | Warsaw | 300 |
| UA0870 | London | Washington | 800 |

### Syntax
* základní operátory: výběr (selekce), projekce, sjednocení, rozdíl množin, kartézský součin, přejmenování
* Operátory berou jednu nebo více relací jako vstup a vrací novou relaci jako
výsledek.
- booleovské operace $\cap, \cup, \setminus, All$
- kartézský součin $\times$
- Selekce $\sigma_{\varphi}(R)$, kde $\varphi$ je bool výraz. Selekce vybere
všechny uspořádané n-tice z relace $R$, pro které podmínka platí.
- Projekce $\pi_{u_1...u_n}(R)$ vrací z relace $R$ atributy $u_1...u_n$ v daném
pořadí.
- Natural join $R\bowtie S$ spojí dvě relace na společném atributu.
- Příklad:
- $\sigma_{\text{from}='Prague'}(R)$

| flight | from | to | price |
| ------ | :----: | --------: | ----: |
| LH8302 | Prague | Frankfurt | 240 |
- $\pi_{price, flight}\sigma_{\text{from}='Prague'}(R)$

| price | flight |
| ----- | :----: |
| 240 | LH8302 |
- Tady si to můžete vyzkoušet interaktivně 👉 <http://mufin.fi.muni.cz/projects/PA152en/relalg/>.

## Datalog

- zjednodušená verze Prologu, která byla vyvinuta pro práci s databázemi.
- nemá funkční symboly, řezy, negace apod.
- Datalogový program se skládá z množiny Hornových klauzulí:
- $p_0(\bar{X}) ← q_{0,0}(\bar{X}, \bar{Y}) ∧ ... ∧ q_{0,m_0}(\bar{X}, \bar{Y})$
⋮
$p_n(\bar{X}) ← q_{n,0}(\bar{X}, \bar{Y}) ∧ ... ∧ q_{n,m_n}(\bar{X}, \bar{Y})$

kde $p_0, ..., p_n$ jsou nové relace a $q_ij$ jsou relace z databáze nebo
některé nově utvořené relace z $p_0, ..., p_n$

query definovaná datalogovým programem mapuje databázi na relace $p_0, ..., p_n$ definované příslušnými formulemi

### Evaluace

- Začni s prázdnými relacemi $p_0 = \emptyset, ..., p_n = \emptyset$.
- Aplikuj každé pravidlo z programu a přidej n-tice do relací.
- Opakuj dokud nevzniknou další relace.
- Příklad:
- 
- Nejdříve přidáme do $\text{path}$ všechny hrany pomocí prvního pravidla.
- 
- Druhé pravidlo nám říká, že pokud tam existuje tranzitivita mezi $X$ a $Y$
přes $Z$, tak tam přidej $(X, Y)$.
- 
- Opět aplikujeme druhé pravidlo.
- 
- Už nelze aplikovat žádné pravidlo, končíme.
- Další příklad:
- Mějme databázové schéma zadané takto:
`Movie(title, year, length, inColor, studionName, producer)`
- Chceme vrátit herce, kteří hráli v barevných filmech v roce 1950. Datalogový
program v nějáké implementaci by mohl vypadat takto:
- `MoviesColor50(t, y) :- Movie(t, y, l, c, s, p) AND y='1950' AND c='true'`
- Více na [wiki](https://en.wikipedia.org/wiki/Datalog).

## Modální logika

- jedná se o rozšíření predikátové logiky o tzv. modality (zahrnující výrazy
jako jsou "**je možné, je nutné, je nemožné**")
- používá se v přechodových systémech, což jsou orientované grafy:
- $\mathfrak{S}=\left\langle S,\left(E_{a}\right)_{a \in A},\left(P_{i}\right)_{i \in I}, s_{0}\right\rangle$, kde
- $S$ je množina stavů
- $s_0$ je počáteční stav
- $E$ je množina hran, kde každá hrana má danou "akci" $a$ (označení (label) hrany); $E_{a}$ kde "edge colours" $a \in A$ "akce"
- $P$ množina unárních predikátů určující vlastnosti stavů; $P_{i}$ kde "vertex colours" $i \in I$ "vlastnosti"
- mluvíme o "stavech", protože se mnohdy bavíme o stavech nějakého
počítačového systému, programu, ...
- využívá se ve formální verifikaci, grafových databázích, constraint
satisfaction, ...
- Syntax:
- $\square\varphi$ - musí platit $\varphi$, vždy platí $\varphi$, ...
- $\mathcal{G}, s \vDash \square\varphi$ platí iff pro všechny $s\to t$, pro
které platí $\mathcal{G}, t \vDash \varphi$ (s a t jsou stavy, $s\to t$ je přechod ze stavu $s$ do stavu $t$)
- $\LARGE\diamond\normalsize\varphi$ - může platit $\varphi$, někdy platí
$\varphi$, ...
- $\mathcal{G}, s \vDash \LARGE\diamond\normalsize\varphi$ platí iff existuje $s\to t$
platí $\mathcal{G}, t \vDash \varphi$
- Příklad:
- $P\wedge \LARGE\diamond\normalsize Q$ - Ve stavu platí $P$ a existuje přechod do stavu kde platí $Q$
- $[a] \perp$ stav nemá žádný vystupní a-přechod
- v teoretické informatice se setkáváme s temporální logikou, tedy stavy
popisují nějáký čas (diskrétní nebo spojitý)
- Příklady formulí temporální logiky:
- $P$ nikdy neplatí
- $\square\neg P$
- Po každém $P$ existuje nějaké $Q$
- $\square(P \to \LARGE\diamond\normalsize Q)$
- Až bude platit $P$, pak bude platit napořád
- $\square(P \to \square P)$
- Existuje nekonečně mnoho P
- $\square\LARGE\diamond\normalsize P$

### Bisimulace

- viz [(1)](http://web.mit.edu/cdg/www/teaching/modal%20logic%20guest%20lecture%2010-26.pdf), [(2)](https://en.wikipedia.org/wiki/Bisimulation), [(3)](https://staff.fnwi.uva.nl/d.j.n.vaneijck2/courses/lai0506/LAI11.pdf)
- Každou formuli ve výrokové modální logice $\varphi$ můžeme převést na formuli
predikátové logiky $\varphi^{*}(x)$, ale ne naopak => modální logika je tedy slabší. Převedeme takto:


- Důkaz:

- Abychom ukázali, kdy je formule predikátové logiky ekvivalentní s formulí
modální logiky, zavedeme si nejprve pojem *bisimulace*, která slouží k
porovnávání dvou přechodových systémů.
- Nechť $\mathcal{S}$ a $\mathcal{T}$ jsou přechodové systémy:
- Bisimulace je relace $Z \subseteq S \times T$ pokud pro každou dvojici
$(s, t) \in Z$ platí:
- $s \in P \iff t \in P$ stavy mají stejné vlastnosti
- pro každou hranu $s \to s'$ existuje $t \to t'$, kde $(s', t') \in Z$
- pro každou hranu $t \to t'$ existuje $s \to s'$, kde $(s', t') \in Z$
- stavy $\mathcal{S}, s$ a $\mathcal{T},t$ jsou bisimilární, pokud existuje
bisimulace $Z$, kde $(s, t) \in Z$
- Na první pohled to může připomínat isomorfismus, ale bisimulace je slabší;
isomorfismus vyžaduje např. stejný počet stavů (a v kontextu zkoumání
přechodových systémů to může být overkill).
- příklad:
- 
- přerušované čáry je bisimulace
- Dva konečné přechodové systémy $\mathcal{S}$ a $\mathcal{T}$ jsou bisimilární
iff platí
$$
\mathcal{S} \vDash \varphi \iff \mathcal{T} \vDash \varphi
\text{, pro každou modální formuli } \varphi
$$
- Formule $\varphi(x)$ je bisimulation invariant pokud platí, že
$$
\mathcal{G, s} \sim \mathcal{T, t} \text{ implies } \mathcal{S} \vDash
\varphi(s) \iff \mathcal{T} \vDash \varphi(t)
$$
- Takže formule v predikátové logice je ekvivalentní s modální formulí iff je bisimulation invariant.

## Temporální logiky

- Motivace: předešlá modální logika je příliš slabá; pro praktické účely si ji rozšíříme.

### Linear Temporal Logic (LTL)

- viz <https://en.wikipedia.org/wiki/Linear_temporal_logic>
- 
- od obyčejné modální logiky se liší:
- $\varphi U \psi$ - platí pokud $\varphi$ platí než narazíme na $\psi$
- finally $F\varphi := \intercal U\psi$ - nezajímá nás, co se děje před $\psi$
- generally $G\varphi := \neg F \neg \varphi$ všude platí $\varphi$
- 
- formule z LTL můžeme převádět do predikátové logiky a do regulárních výrazů
bez hvězdičky

### Computation Tree Logic (CTL and CTL*)

- viz <https://en.wikipedia.org/wiki/Computation_tree_logic>
- 
- state formulae máme pro výběr větví
- $A$ všechny větve
- $E$ existuje v nějáké větvi
- path formulae máme pro cestu

<!--
### $\mu$-calculus ($L_\mu$)

- viz <https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus>
- 

-->

## Tablové důkazy ve výrokové, predikátové a modální logice

- dokazovací metoda, pomocí které můžeme dokázat pravdivost či splnitelnost
formulí
- Postup:
- 
- tedy opět dokazujeme sporem:
- formuli, kterou chceme dokázat, přiřadíme `false`
- pomocí pravidel chceme dojít ke kontradikci
- pokud jsou všechny větve kontradikce, pak je formule pravdivá
- pokud pouze jedna větev je kontradikce, pak je formule splnitelná
- to, že je větev kontradikce znamená, že ve větvi existuje pro nějakou
formuli $\psi$ $\psi true$ a zároveň $\psi false$

### Výroková logika a predikátová logika

- Pravidla:
- 
- Příklady:
- 
- 

### Modální logika

- Postup
- 
- Pravidla
- 
- 
- Příklady
- 
- 
- 

## Přirozená dedukce

- 
- 
- Pravidla pro výrokovou logiku
- 
- Příklad pro výrokovou logiku
- 
- Pravidla pro predikátovou logiku
- 
- Příklad
- 

## Induktivní inference ve výrokové a predikátové logice

- indukce je proces hledání obecných hypotéz na základě pozorovaných dat
- např. na základě dat, chceme umět predikovat kategorii apod.
- v kontextu logiky budeme chtít umět najít hypotézu, která aproximuje nějakou
booleovskou funkci na pozorovaných datech:
- pozorovaná (trénovací data) $(x_1, y_1), ..., (x_n, y_n)$
- chceme aproximovat $f:\{0, 1\}^n \to \{0, 1\}$, konkrétně $y_i = f(x_i)$
- hledáme tedy takovou hypotézu, aby $h(x) \approx f(x)$
- příklad:
- 
- chceme predikovat `EnjoySport` na základě ostatních atributů
- hypotézu hledáme v prostoru hypotéz
- příklad hypotézy pro náš problém $(?, \text{Cold}, \text{High}, ?, ?, ?)$
- tj. `AirTemp` musí být `Cold`, `Humidity` musí být `High`, `?` označuje
libovolnou hodnotu
- jedná se o konjuktivní hypotézu, protože musí být splněny všechny
podmínky hypotézy
- hypotézy lze částečně seřadit podle jejich specificity (general-to-specific
ordering)
- $h_1 = (\text{Sunny}, ?, ?, \text{Strong}, ?, ?)$
- $h_2 = (\text{Sunny}, ?, ?, ?, ?, ?)$
- $h_2$ má méně podmínek a všechny pozitivní příklady, které označí $h_1$,
$h_2$ označí stejným způsobem, je tedy obecnější (general); naopak $h_1$ je
více specifická
- hypotéza je konzistentní pokud $h(x) = f(x)$ pro pozorovaná data
- obecně preferujeme jednodušší hypotézu - Ockhamova břitva

### Hledání hypotéz

- nejnaivnější způsob je brute-force hledání v prostoru hypotéz (enumerace)
- jeden z nejjednodušších způsobů je využití častečnému seřazení podle
specificity a hledat od nejspecifictější hypotézy a postupně generalizovat
- Find-S algoritmus
- 
- 
- pokud nalezena nejspecifičtější hypotéza zahrnuje i negativní příklady,
pak neexistuje konzistentní konjunktivní hypotéza
- nedostatky:
- ignoruje negativní příklady a nekontroluje tím pádem konzistenci
- náchylný na špatně anotované data (inkonzistentní data můžou velmi
ovlivnit výsledek)
$\cup$
- další způspb je vypočítat tzv. prostor verzí - množinu hypotéz, které jsou
s daty konzistentní:
- to uděláme pomoci algoritmu Candidate-Elimination, který spočítá
nejobecnější a nejspecifičtější konzistentní hypotézy
- 
- 
- viz
- [Machine Learning od Toma Mitchella, kapitola 2](http://www.cs.ubbcluj.ro/~gabis/ml/ML-books/McGrawHill%20-%20Machine%20Learning%20-Tom%20Mitchell.pdf)
- [PV056, vicemene vycuc z predesle kapitoly](https://is.muni.cz/auth/el/fi/jaro2019/PV056/um/62159239/ml-classification.pdf)
- [AI2 z Matfyzu, kapitola 19 z Modern approach to AI](http://ktiml.mff.cuni.cz/~bartak/ui2/lectures/lecture10.pdf)