Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| statnice:bakalar:b0b01lgr [2025/05/19 12:49] – [Úplné systémy logických spojek] zapleka3 | statnice:bakalar:b0b01lgr [2025/06/01 11:45] (current) – zapleka3 | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ==== Syntaxe a sémantika výrokové a predikátové logiky. Základní pojmy teorie grafů. ==== | + | ====== Syntaxe a sémantika výrokové a predikátové logiky. Základní pojmy teorie grafů. |
| [[https:// | [[https:// | ||
| Line 132: | Line 132: | ||
| Ohodnocení formule určuje její pravdivost ve specifickém světě – tedy za konkrétní přiřazení hodnot 0 a 1 jednotlivým proměnným. Například pro formuli $(a \land b)$ je její hodnota 1 pouze tehdy, když $a = 1$ a $b = 1$. | Ohodnocení formule určuje její pravdivost ve specifickém světě – tedy za konkrétní přiřazení hodnot 0 a 1 jednotlivým proměnným. Například pro formuli $(a \land b)$ je její hodnota 1 pouze tehdy, když $a = 1$ a $b = 1$. | ||
| - | |||
| - | |||
| - | |||
| - | |||
| ==== Důsledek ve výrokové logice ==== | ==== Důsledek ve výrokové logice ==== | ||
| Line 169: | Line 165: | ||
| * $\{ \alpha ⇒ \beta, \beta ⇒ \gamma \} \models (\alpha ⇒ \gamma)$ | * $\{ \alpha ⇒ \beta, \beta ⇒ \gamma \} \models (\alpha ⇒ \gamma)$ | ||
| - | **Rezoluční metoda** (alternativa pro důkaz nesplnitelnosti množiny formulí v CNF): | ||
| - | * Převeď formule na CNF, vytvoř množinu klausulí | ||
| - | * Opakuj aplikaci rezoluce na dvojice klausulí | ||
| - | * Pokud vznikne prázdná klausule (označena $F$), množina je nesplnitelná | ||
| - | * Rezoluční metoda se často používá pro **automatizovaný důkaz nesplnitelnosti** – například v oblastech jako **SAT solving**, ověřování softwaru nebo **umělá inteligence**. | ||
| - | |||
| - | **Doporučený postup**: Postupně eliminuj proměnné pomocí rezoluce, až zbude buď prázdná množina (splnitelnost), | ||
| ==== Úplné systémy logických spojek ==== | ==== Úplné systémy logických spojek ==== | ||
| Line 205: | Line 194: | ||
| Další nástroje: | Další nástroje: | ||
| - | * **Rezoluční metoda** pro ověření splnitelnosti množiny klausulí (v CNF) | ||
| * **Syntaktické důsledky** pomocí přirozené dedukce nebo Hilbertova systému | * **Syntaktické důsledky** pomocí přirozené dedukce nebo Hilbertova systému | ||
| + | * **Rezoluční metoda** (alternativa pro důkaz nesplnitelnosti množiny formulí v CNF): | ||
| + | * Převeď formule na CNF, vytvoř množinu klausulí | ||
| + | * Opakuj aplikaci rezoluce na dvojice klausulí | ||
| + | * Pokud vznikne prázdná klausule (označena $F$), množina je nesplnitelná | ||
| + | * Rezoluční metoda se často používá pro **automatizovaný důkaz nesplnitelnosti** – například v oblastech jako **SAT solving**, ověřování softwaru nebo **umělá inteligence**. | ||
| + | |||
| + | **Doporučený postup**: Postupně eliminuj proměnné pomocí rezoluce, až zbude buď prázdná množina (splnitelnost), | ||
| + | |||
| {{: | {{: | ||
| Line 248: | Line 244: | ||
| **Platí**: | **Platí**: | ||
| - | * $\varphi | + | * $\varphi \models \psi$ právě když $(\varphi \Leftrightarrow \psi)$ je tautologie. |
| * Např. $\neg \forall x\, P(x) \models\!\models \exists x\, \neg P(x)$ | * Např. $\neg \forall x\, P(x) \models\!\models \exists x\, \neg P(x)$ | ||
| Line 267: | Line 263: | ||
| * Zachovává **ekvisplnitelnost**, | * Zachovává **ekvisplnitelnost**, | ||
| - | {{: | ||
| ==== Důsledek v predikátové logice ==== | ==== Důsledek v predikátové logice ==== | ||
| Line 289: | Line 284: | ||
| * Odvozovací systém bez axiomů, používá pravidla pro spojky i kvantifikátory | * Odvozovací systém bez axiomů, používá pravidla pro spojky i kvantifikátory | ||
| * Dedukce: $S \vdash \varphi$ znamená, že $\varphi$ lze odvodit ze $S$ | * Dedukce: $S \vdash \varphi$ znamená, že $\varphi$ lze odvodit ze $S$ | ||
| + | |||
| + | {{: | ||
| **Věta o úplnosti**: | **Věta o úplnosti**: | ||
