commit f506747792956723a5906c63c22422405dd22227 Author: mark Date: Tue Aug 12 16:33:24 2025 +0200 ah yes diff --git a/README.md b/README.md new file mode 100644 index 0000000..613205f --- /dev/null +++ b/README.md @@ -0,0 +1,270 @@ +# Aussagenlogik + +## Aussagenlogische Formeln (Syntax) + +- $A_1, A_2, \dots$ bzw. $A, B, C$ : atomare Formeln +- $0$, $1$ : Boolesche Konstanten +- $\lnot F$ : Negation von $F$ +- $(F \land G)$ : Konjunktion +- $(F \lor G)$ : Disjunktion +- $(F \to G)$ : entspricht $(\lnot F \lor G)$ +- $(F \leftrightarrow G)$ : entspricht $((F \land G) \lor (\lnot F \land \lnot G))$ +- $(\bigvee_{i=1}^n F_i)$ : entspricht $((F_1 \lor F_2) \lor F_3) \dots$ +- $(\bigwedge_{i=1}^n F_i)$ : entspricht $((F_1 \land F_2) \land F_3) \dots$ + +Klammern weglassen: $\land$ bindet stärker als $\lor$, also $a \land b \lor c \iff (a \land b) \lor c$ + +## Belegung (Semantik) + +Eine Belegung $\mathcal A$ legt für jede atomare Formel ($A_1, A_2, \dots, B, C, \dots$) einen Wahrheitswert, z.B. $\mathcal A(A_1) = 0$, fest. + +Außerdem: $\mathcal A(F)$ ist der Wahrheitswert der Formel $F$ unter der Belegung $\mathcal A$, d.h. +der Wahrheitswert der Formel $F$, wenn alle atomaren Formeln, z.B. $A_1, \dots, A_n$, als $\mathcal A(A_1), \dots, \mathcal A(A_n)$ gedeutet werden. + +In diesen Definitionen wird dann die Semantik festgelegt: +$\land$ ist das *Und*, $\lor$ ist das *Oder*, und $\lnot$ ist die *Negation*. + +## Definitionen + +Falls eine Belegung $\mathcal A$ für alle in einer Formel $F$ vorkommenden +atomaren Formeln definiert ist, so heißt $\mathcal A$ zu $F$ **passend** (d.h. einfach: man kann $\mathcal A$ auf $F$ anwenden). + +Gilt $\mathcal A(F) = 1$, dann ist $\mathcal A$ ein **Modell** für $F$: $\mathcal A \; |= \; F$. + +Eine *Menge von Formeln* heißt erfüllbar, falls es eine Belegung $\mathcal A$ gibt, die für *jede* der Formeln ein Modell ist. + +Eine Formel $F$ heißt **gültig** oder **Tautologie** falls jede passende Belegung ein Modell für $F$ ist: $|= \; F$ + +$F$ ist gültig genau dann, wenn $\lnot F$ unerfüllbar ist. + +Folgt $G$ logisch aus $F$ (**logische Folgerung**), $F \; |= \; G$, gilt $|= \; F \to G$ + +Wenn es mindestens ein Modell für $F$ gibt, heißt $F$ **erfüllbar**, sonst **unerfüllbar**. + +## Erfüllbarkeit und Gültigkeit Prüfen + +Man könnte "einfach" alle $2^n$ Belegungen ausprobieren. + +## Semantische Äquivalenz (Syntaktisch unterschiedlicher Formeln) + +Zwei Formeln $F$ und $G$ sind **semantisch äquivalent**, wenn sie unter +jeder (passenden) Belegung denselben Wahrheitswert erhalten: $F \equiv G$ + +Es gilt $F \equiv G$ genau dann, wenn $|= \; (F \leftrightarrow G)$ gilt. + +Semantische Äquivalenzen: + +- Idempotenz + + $F \land F \equiv F$ + + $F \lor F \equiv F$ +- Kommutativität + + $F \land G \equiv G \land F$ + + $F \lor G \equiv G \lor F$ +- Assoziativität + + $F \land (G \land H) \equiv (F \land G) \land H$ + + $F \lor (G \lor H) \equiv (F \lor G) \lor H$ +- Distributivgesetz + + $F \land (G \lor H) \equiv (F \land G) \lor (F \land H)$ + + $F \lor (G \land H) \equiv (F \lor G) \land (F \lor H)$ +- Absorptionsgesetze + + $F \land (F \lor G) \equiv F$ + + $F \lor (F \land G) \equiv F$ +- deMorgan + + $\lnot (F \lor G) = \lnot F \land \lnot G$ + + $\lnot (F \land G) = \lnot F \lor \lnot G$ +- Doppelnegation + + $\lnot \lnot F \equiv F$ +- Tautologie- und Unerfüllbarkeitsregeln + + $1 \lor G \equiv 1$ + + $0 \lor G \equiv G$ + + $1 \land G \equiv G$ + + $0 \land G \equiv 0$ + + statt 0 oder 1 auch tautologien oder unerfüllbare Formeln möglich + +## Konjunktive und Disjunktive Normalformen (KNF/DNF) + +Beispiels-KNF: \ +$F = (A \lor \lnot B) \land (\lnot C \lor \lnot A \lor D) \land (\lnot A \lor \lnot B) \land D \land \lnot E$ + +Beispiels-DNF: \ +$F = (A \land \lnot B) \lor (\lnot C \land \lnot A \land D) \lor (\lnot A \land \lnot B) \lor D \lor \lnot E$ + +Für jede Formel $F$ gibt es (mind.) eine äquivalente ($\equiv$) Formel in KNF und (mind.) eine in DNF. + +## Hornformeln + +Erfüllbarkeit mit beliebigen Formeln oder KNFs zu prüfen ist schwierig (NP), +mit DNFs ist es aber einfach - DNFs herzustellen ist aber schwierig. + +Hornformeln sind eingeschränkte aussagenlogische Formeln, +deren Erfüllbarkeit dafür aber leicht zu testen ist. + +Hornformeln sind Formeln $F$ in KNF, wobei jede Klausel in $F$ +höchstens ein positives Literal enthält: + +Hornklauseln: $A$, $\lnot A$, $\lnot A \lor B$, $\lnot A \lor B \lor \lnot C$, aber **nicht** $A \lor B$, $\lnot A \lor B \lor C$ + +Hornformel: $A \land (\lnot A \lor B) \land \lnot C$ + +(TODO?) Erfüllbarkeitstest für Hornformeln (Aussagenlogik2:21) + +## Resolution + +Mit Resolution kann eine Formel auf Unerfüllbarkeit getestet werden. + +Basierend nur auf Syntax wissen wir u.A.: + +- $F \lor \lnot F \equiv 1$ und $F \land \lnot F \equiv 0$ +- Wenn $F$ und $F \to G$, dann auch $G$ + +**Anwendung:** + +Sei $F$ eine Formel in KNF, also + +$F = (L{1,1} \lor \dots \lor L_{1,n_1}) \land \dots \land (L_{k,1} \lor \dots \lor L_{k,n_k})$ + +Wir stellen die Formel als Mengen von Klauseln dar: + +$F = \{ \{ L_{1,1}, \dots, L_{1,n_1} \}, \dots, \{ L_{k,1}, \dots, L_{k,n_k} \} \}$ + +Wenn es zwei Klauseln gibt, wovon eine ein Literal positiv und die andere dasselbe Literal negativ beinhaltet, +wird $R$ aus den beiden Klauseln nach dem Literal resolviert: + +$K_1 = \{ A, \lnot B, C, D \}$ \ +$K_2 = \{ A, \lnot B, \lnot C \}$ \ +$\to \{ A, \lnot B, D } = R$ + +Also $R = K_1$ ohne $C \; \cup \; K_2$ ohne $\lnot C$ + +Wenn man irgendwie auf einen Resolvent $R = \{ \}$ kommt, +ist die Formel widerlegt (Resolutionssatz der Aussagenlogik). + +# Prädikatenlogik + +Erweitert die Aussagenlogik mit + +- Quantoren $\exists, \forall$ +- Variablen $x_1, x_2, \dots$ oder $u, v, w, x, y, z$ +- Funktions- und Prädikatssymbole $f_1, f_2, \dots$ oder $f, g, h$ +- Konstanten (Funktionssymbole der Stelligkeit 0): $a_1, a_2, \dots$ oder $a, b, c$ +- Prädikatsybole: $P_1, P_2, \dots$ oder $P, Q, R$ + +## Signatur + +$\Sigma = \{ a/0, f/3, P/2 \}$ + +Beinhaltet nicht die Variablen + +$PL(\Sigma)$ ist die Menge aller prädikatenlogischen *Aussagen* über der Signatur $\Sigma$. + +## Prädikatenlogische Formeln + +### Terme + +- Variablen $x_1$ +- Funktionen $f(t_1, \dots, t_k)$ mit *Termen* $t_1, \dots, t_k$ + +Terme, die keine Variablen enthalten, sind **Grundterme**. + +### Formeln + +- $P(t_1, \dots, t_k)$ mit *Termen* $t_1, \dots, t_k$ und Prädikatsymbol $P$ (Atomare Formeln) +- Sonst wie bei Aussagenlogik mit $\lnot$, $\land$, $\lor$ +- $\exists x F$ und $\forall x F$ mit Variable $x$ und Formel $F$ + +--- + +Variablen sind *gebunden*, wenn sie mit $\exists$ oder $\forall$ verwendet werden, sonst *frei*. + +Eine Formel ohne Vorkommen einer freien Variable heißt *geschlossen* oder eine *Aussage*. + +## Matrix + +Die Matrix von $F$, also $F$ ohne $\exists$ und $\forall$, ist $F^*$: + +$F = \exists x \dots \land \lnot \forall y \dots$ \ +$F^* = \dots \land \lnot \dots$ + +## Bereinigt + +Eine Formel ist bereinigt, wenn verschiedene Quantoren nicht dieselbe Variable binden: + +$\exists x \dots \land \forall x \dots \; \to \; \exists x \dots \land \forall y \dots$ + +## Struktur $\mathcal A$ + +Eine Struktur $\mathcal A$ zu einer Signatur $\Sigma$ ist ein Paar $(U_{\mathcal A}, I_{\mathcal A})$. + +$U_{\mathcal A}$ ist das Universum, $I_{\mathcal A}$ ordnet jedem Funktions-/Prädikatssymbol eine Funktion bzw. Relation (Menge) auf $U_{\mathcal A}$ zu. + +Wir schreiben $f^{\mathcal A}$ für $I_{\mathcal A}(f)$ bzw $P^{\mathcal A}$ für $I_{\mathcal A}(P)$. + +Eine Struktur ist **passend** zu einer Aussage, falls die Signatur passt (d.h. die in $F$ vorkommenden Funktions-/Prädikatssymbole Elemente von $\Sigma$ sind). + +### Auswertung mit Variablen + +$\mathcal A [x/m]$ bedeutet, dass die Variable $x$ den Wert $m$ annimmt. + +## Modell, Erfüllbarkeit, Äquivalenz, \dots + +Eine Struktur $\mathcal A$ ist ein Modell für $F$ ($\mathcal A |= F$) wenn wahr (wie bei AL). + +Auch wie bei AL: Erfüllbarkeit, (allgemeine) Gültigkeit, Äquivalenz, Logische Folgerung. \ +Äquivalenzen aus der AL gelten auch in der PL. + +## Pränexform + +Alle Quantoren am Anfang, also z.B. +$\exists x \forall y \exists z H$. + +Für jede Formel gibt es eine äquivalente (und bereinigte) Formel in Pränexform. + +Dazu: Formel bereinigen, dann Quantoren einfach rausziehen, sodass innere Quantoren nach äußeren stehen. + +## Skolemform + +Sei $F$ eine Formel in bereinigter Pränexform. +Man erhält nun die Skolemform von $F$, indem man +$\forall x_1 \dots \forall x_n \exists x_{n+1} G$ in $\forall x_1 \dots \forall x_n G [x_{n+1}/f(x_1,\dots,x_n)]$ +umwandelt, d.h. man je den **ersten** Existenzquantor $\exists$ entfernt und dessen Variable als Funktion der äußeren Variablen (aus davor stehenden $\forall$) schreibt. +Diese Funktion $f$ kann auch nullstellig sein, also eine Konstante, z.B. $a$. + +Ist $F$ geschlossen, so gilt: $F$ ist genau dann erfüllbar, wenn die Skolemform von $F$ erfüllbar ist. + +$\to$ **Matrix der Skolemform in KNF als Klauselmenge, dann Resolution** + +## Herbrand-Universum + +Das Herbrand-Universum $D(F)$ einer geschlossenen Formel $F$ in Skolemform +ist die Menge aller variablenfreien Terme, die aus den Bestandteilen von $F$ +gebildet werden können: + +- Alle Konstanten aus $F$ sind in $D(F)$ +- $f(t_1, \dots, t_n)$ ist in $D(F)$, mit $f \in F$ und $t_1, \dots, t_n$ \in $D(F)$ + +## Herbrand-Struktur + +$(D(F), f^{\mathcal A} \mapsto f)$ + +Wahl für $P$ etc ist noch offen. + +Mit Limitierung auf Herbrand-Strukturen immernoch **erfüllbarkeitsäquivalent**. + +## Satz von Löwenheim-Skolem + +Jede erfüllbare Formel der Prädikatenlogik besitzt bereits ein abzählbares Modell. + +Da $\mathbb R$ überabzählbar, kann es in PL nicht formuliert werden. + +## Herbrand-Expansion + +Die Herbrand-Expansion $E(F)$ einer Formel $F = \forall \dots F^*$ in Skolemform +ist die Menge aller möglichen Formeln $F^*[\dots][\dots]\dots[\dots]$ mit $\dots \in D(F)$. + +$F$ unerfüllbar genau dann wenn eine endliche Teilmenge von $E(F)$ unerfüllbar ist. + +$\to$ Unerfüllbarkeit ist semi-entscheidbar (Entscheidbarkeit damit co-semi-entscheidbar). + +## Grundresolution + +Resolution wie bei AL, basierend auf Herbrand-Expansion