The wiki page is under active construction, expect bugs.

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
statnice:bakalar:b0b01lgr [2025/05/19 12:24] – [Normální formy formulí] zapleka3statnice: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://fel.cvut.cz/cz/education/bk/predmety/46/80/p4680706.html|B0B01LGR]] [[https://math.fel.cvut.cz/en/people/gollova/lgr/lgr-prednaska.html|Webové stránky předmětu]] [[https://docs.google.com/document/d/1yGhEceIZR0vuSbkH2nP-3HrXwGxUGZck/edit|Manuál 101]] [[https://fel.cvut.cz/cz/education/bk/predmety/46/80/p4680706.html|B0B01LGR]] [[https://math.fel.cvut.cz/en/people/gollova/lgr/lgr-prednaska.html|Webové stránky předmětu]] [[https://docs.google.com/document/d/1yGhEceIZR0vuSbkH2nP-3HrXwGxUGZck/edit|Manuál 101]]
Line 114: Line 114:
  
 **Disjunktivní normální forma (DNF)**: **Disjunktivní normální forma (DNF)**:
-  * formule tvořená disjunkcí mintermů+  * formule tvořená disjunkcí mintermů, minterm je literál nebo konjunkce konečně mnoha literálů
   * vhodná pro přímé zápisy splnitelných funkcí   * vhodná pro přímé zápisy splnitelných funkcí
  
 **Konjunktivní normální forma (CNF)**: **Konjunktivní normální forma (CNF)**:
-  * formule tvořená konjunkcí maxtermů+  * formule tvořená konjunkcí maxtermů, maxterm je literál nebo disjunkce konečně mnoha literálů
   * vhodná pro důkaz nesplnitelnosti (např. rezoluční metodou)   * vhodná pro důkaz nesplnitelnosti (např. rezoluční metodou)
  
Line 126: Line 126:
 Každé zobrazení $f: \{0,1\}^n \to \{0,1\}$ lze vyjádřit jako výrokovou formuli v CNF i DNF. Každé zobrazení $f: \{0,1\}^n \to \{0,1\}$ lze vyjádřit jako výrokovou formuli v CNF i DNF.
  
 +**Booleovské operace** (pro hodnoty $\{0,1\}$):
 +  * $x \cdot y = \min(x, y)$
 +  * $x + y = \max(x, y)$
 +  * $\bar{x} = 1 - x$
 +
 +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 131: Line 137:
 Formule $\psi$ je **sémantickým důsledkem** formule $\varphi$, značíme $\varphi \models \psi$, pokud každé ohodnocení, které splňuje $\varphi$, splňuje i $\psi$. Formule $\psi$ je **sémantickým důsledkem** formule $\varphi$, značíme $\varphi \models \psi$, pokud každé ohodnocení, které splňuje $\varphi$, splňuje i $\psi$.
  
-**Důležitá tvrzení:** +**Syntaktický důsledek vs. sémantický důsledek**: 
-  * $\varphi \models \psi$ právě tehdy, když $(\varphi ⇒ \psi)$ je tautologie +  * $\varphi \vdash \psi$ znamená, že $\psi$ lze **formálně odvodit** z $\varphi$ pomocí pravidel dedukce (např. přirozené dedukce nebo Hilbertova systému). 
-  * Množina $S \models \varphi$ právě tehdy, když $S ∪ \{\neg \varphi\}$ je nesplnitelná +  * $\varphi \models \psi$ znamená, že ve **všech ohodnoceních**, kde je $\varphi$ pravdivá, je pravdivá i $\psi$. 
-  * $S ∪ \{\varphi\} \models \psi \iff S \models (\varphi ⇒ \psi)$+  * Platí: pokud $\varphi \vdash \psi$, pak $\varphi \models \psi$ (správnost systému); opačně platí v úplných systémech (úplnost). 
 + 
 +**Formální definice**: 
 +  * Mějme množinu formulí $S$ a ohodnocení $u: P(A) \to \{0, 1\}$. 
 +    * $S$ je **pravdivá v ohodnocení** $u$, pokud $u(\varphi) = 1$ pro každou $\varphi \in S$. 
 +    * $S$ je **nepravdivá v ohodnocení** $u$, pokud existuje alespoň jedna $\varphi \in S$, pro kterou $u(\varphi) = 0$. 
 +    * $S$ je **splnitelná**, pokud existuje alespoň jedno ohodnocení $u$, ve kterém je všechno z $S$ pravdivé. 
 +    * $S$ je **nesplnitelná**, pokud žádné takové ohodnocení neexistuje. 
 + 
 +**Definice důsledku**: 
 +  * Formule $\varphi$ je **důsledkem množiny** $S$, značíme $S \models \varphi$, právě tehdy, když každé ohodnocení, které splňuje všechny formule v $S$, splňuje i $\varphi$. 
 + 
 +**Důležitá tvrzení**: 
 +  * $\varphi \models \psi$ právě tehdy, když $(\varphi ⇒ \psi)$ je tautologie. 
 +  * $S \models \varphi$ právě tehdy, když množina $S ∪ \{\neg \varphi\}$ je nesplnitelná. 
 +  * $S ∪ \{\varphi\} \models \psi$ právě tehdy, když $S \models (\varphi ⇒ \psi)$. 
 + 
 +**Příklad**: 
 +Mějme $S := \{a, a ⇒ b\}$ a $M := b$.   
 +Všechna ohodnocení, která splňují $S$, splňují i $b$. Proto $S \models M$.
  
 **Příklady:** **Příklady:**
Line 140: 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), nebo $F$ (nesplnitelnost) 
  
 ==== Úplné systémy logických spojek ==== ==== Úplné systémy logických spojek ====
Line 164: Line 182:
   * $(a ∨ b) ≡ (\neg a ⇒ b)$   * $(a ∨ b) ≡ (\neg a ⇒ b)$
   * $(a ∧ b) ≡ \neg(a ⇒ \neg b)$   * $(a ∧ b) ≡ \neg(a ⇒ \neg b)$
- 
-**Booleova algebra**: 
-  * Základní operace: $x \cdot y$, $x + y$, $\bar{x}$ 
-  * Každá Booleova funkce má ekvivalentní formuli v DNF i CNF 
  
 ==== Schopnost formalisace a řešení logických úloh ==== ==== Schopnost formalisace a řešení logických úloh ====
Line 180: 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), nebo $F$ (nesplnitelnost)
 +
  
 {{:statnice:bakalar:pasted:20250517-191116.png}} {{:statnice:bakalar:pasted:20250517-191116.png}}
Line 223: Line 244:
  
 **Platí**: **Platí**:
-  * $\varphi \models\!\models \psi$ právě když $(\varphi \Leftrightarrow \psi)$ je tautologie.+  * $\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 242: Line 263:
   * Zachovává **ekvisplnitelnost**, ale ne tautologickou ekvivalenci.   * Zachovává **ekvisplnitelnost**, ale ne tautologickou ekvivalenci.
  
-{{:statnice:bakalar:pasted:20250517-201056.png}} 
  
 ==== Důsledek v predikátové logice ==== ==== Důsledek v predikátové logice ====
Line 264: 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$
 +
 +{{:statnice:bakalar:pasted:20250517-201056.png}}
  
 **Věta o úplnosti**: **Věta o úplnosti**:

Trace: • b4b33alg

Navigation

Playground

QR Code
QR Code statnice:bakalar:b0b01lgr (generated for current page)