Syntaxe

Definice: Jazyk je neprázdná množina výrokových proměnných $\mathbb{P}$, prvkům říkáme prvovýroky nebo atomické výroky. Kromě těchto proměnných máme také logické symboly $\neg ,\wedge ,\vee ,\to ,\leftrightarrow$ a závorky, pro jazyky predikátové logiky přidáváme ještě $\exists ,\forall .$

Definice: Výrok v jazyce $\mathbb{P}$ je prvek množiny ${\text{VF}}_{\mathbb{P}}$ definované jako nejmenší množina splňující

1. $\forall p\in \mathbb{P}:p\in {\text{VF}}_{\mathbb{P}}$,
2. $\forall \phi \in {\text{VF}}_{\mathbb{P}}:\neg \phi \in {\text{VF}}_{\mathbb{P}}$,
3. $\forall \phi ,\psi \in {\text{VF}}_{\mathbb{P}}:\phi \wedge \psi ,\phi \vee \psi ,\phi \to \psi ,\phi \leftrightarrow \psi \in {\text{VF}}_{\mathbb{P}}$.

Vzhledem k tomu, že ne každý prvovýrok musí být obsáhnut v každém výroku tak definujeme $\text{Var}:{\text{VF}}_{\mathbb{P}}\to \mathcal{P}(\mathbb{P})$, která zobrazí $\psi \in {\text{VF}}_{\mathbb{P}}$ na množinu obsahující prvovýroky ve $\psi$.

Definice: Podvýrok (podformule) je podřetězec, který je sám o sobě výrok. Množinu prvovýroků obsažených ve formuli $\phi$ označíme $\mathrm{Var}(\phi )$. Např. pro

$$\phi =((p\vee \neg q)\leftrightarrow (r\to (p\wedge q)))$$

platí $\mathrm{Var}(\phi )=\{p,q,r\}$.

Definice: Každá formule $\phi \in {\mathrm{VF}}_{\mathbb{P}}$ má jedinečný syntaktický strom $\text{Tree}(\phi )$, kde listy jsou atomické výroky $p\in \mathbb{P}$ a vnitřní uzly jsou unární symbol $\neg$ nebo binární symboly $\wedge ,\vee ,\to ,\leftrightarrow$.

Definice: Výskytem proměnné $x$ ve formuli $\psi$, je rozuměno, že existuje list $\text{Tree}(\psi )$ s označením $x$, výskyt je

1. vázaný je-li takové $x$ i součástí nějakého podstromu začínajícího $(Qx)$, kde $Q\in \{\forall ,\exists \}$,
2. volný kdykoliv není vázaný.

Definice: Teorie $T$ v jazyce $\mathbb{P}$ je libovolná množina výrokových formulí $T\subseteq {\mathrm{VF}}_{\mathbb{P}}$. Axiomy teorie jsou prvky $T$.

Definice: Formule je otevřená, pokud neobsahuje žádný kvantifikátor; je to uzavřená (sentence), pokud nemá žádnou volnou proměnnou.

Příklad: $x+y\le 0$ je otevřená; $(\forall x)(\forall y)(x+y\le 0)$ je uzavřená; $(\forall x)(x+y\le 0)$ není ani otevřená, ani uzavřená.

---

Tvary výrokových formulí

Definice: Instance formule $\phi (x_1,\dots ,x_n)$ na termy $t_1,\dots ,t_n$ je formule

$$\phi [x_1:=t_1,\dots ,x_n:=t_n]$$

kde každá volná proměnná $x_i$ je nahrazena termem $t_i$, přičemž se přejmenují vázané proměnné, aby nedošlo ke kolizi.

Definice: Varianta formule je ekvivalentní formule získaná přejmenováním všech vázaných proměnných (α-konverze).

Konjunktivní normální forma (CNF): literál je $p$ nebo $\neg p$, pro $p\in \mathbb{P}$, klauzule je disjunkce ($\vee$) literálů, formule je konjunkcí ($\wedge$) klauzulí (prázdná formule je $\top$).

Disjunktivní normální forma (DNF): elementární konjunkce je konjunkce literálů, formule je disjunkcí elementárních konjunkcí (prázdná formule je $\perp$).

Převod do CNF/DNF:

1. Odstranění ekvivalencí a implikací:

$$\phi \leftrightarrow \psi \sim (\neg \phi \vee \psi )\wedge (\neg \psi \vee \phi ),\phi \to \psi \sim \neg \phi \vee \psi .$$

2. Posunutí negací na literály (De Morgan), odstranění dvojitých negací.
3. Distributivita:

$$\begin{array}{rl}\varphi \wedge (\psi \vee \chi )& \sim (\varphi \wedge \psi )\vee (\varphi \wedge \chi )\text{(pro DNF)},\\ \varphi \vee (\psi \wedge \chi )& \sim (\varphi \vee \psi )\wedge (\varphi \vee \chi )\text{(pro CNF)}.\end{array}$$

Použití: SAT solvery běžně vyžadují CNF; rezoluční metoda pracuje na množinové reprezentaci klauzulí v CNF.

Definice: Formule je v prenexní normální formě (PNF) , je-li ve tvaru

$$(Q_1{x}_1)\dots (Q_n{x}_n){\phi }^{\prime }$$

kde každý $Q_i\in \{\forall ,\exists \}$ a ${\phi }^{\prime }$ je otevřená (otevřené jádro formule).

Lemma: (Bublání kvatifikátorů) Označme $\overline{Q}$ jako doplňkový kvantifikátor ke $Q$. Nechť $\phi ,\psi$ jsou formule a proměnná není volná ve $\psi$ (kdyby byla tak ji v $\psi$ b.ú.n.o. přejmenujeme). Potom platí

$$\begin{array}{rl}\neg (Qx)\phi & \sim (\overline{Q}x)\neg \phi \\ (Qx)\phi \wedge \psi & \sim (Qx)(\phi \wedge \psi )\\ (Qx)\phi \vee \psi & \sim (Qx)(\phi \vee \psi )\\ (Qx)\phi \to \psi & \sim (\overline{Q}x)(\phi \to \psi )\\ \psi \to (Qx)\phi & \sim (Qx)(\psi \to \phi )\end{array}$$

kde všechny jsou sémanticky jasné až na implikaci, kde kvatifikátor je v antecendentu, kdy je nutnost změny kvatifikátoru vzniká jasně z přepisu implikace na disjunkci a sice

$$(Qx)\phi \to \psi \sim \neg (Qx)\phi \vee \psi \sim (\overline{Q}x)\neg \phi \vee \psi \sim (\overline{Q}x)\phi \to \psi .$$

Převod do PNF:

1. Nahrazení podformulí ekvivalentními dle Lemma o bublání kvatifikátorů
2. Přejmenování vázaných proměnných (α-konverze)
3. Opakování dokud všechny kvantifikátory neprojdou na začátek

Výsledkem je ekvivalentní formule v PNF.

Navíc z PNF můžeme udělat skolemizací Skolemovu variantu, kde máme jen všeobecné kvatifikátory. Process skolemizace je vlastně postaven na myšlence, že existence proměnné, aby něco splnila je podmíněna všeobecnými proměnnými před ní a tedy nahrazujeme proměnné s existenčními kvantifikátory iterativně zprava doleva za funkce které mají jako vstup proměnné nalevo od nich. Tedy začíná-li formule $(\exists x)(\forall y)(\exists z)\psi$, tak všechny výskyty $z$ se nahradí za $f(x,y)$ a poté se všechny výskyty $x$ nahradí $g$, tedy konstantou.