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 13:17] – [Důsledek ve výrokové logice] 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 194: 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 237: 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 256: 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 278: 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:

Navigation

Playground

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