ah yes
This commit is contained in:
commit
f506747792
270
README.md
Normal file
270
README.md
Normal file
@ -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 \}$
|
||||
|
||||
<small>Beinhaltet nicht die Variablen</small>
|
||||
|
||||
$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
|
||||
Loading…
x
Reference in New Issue
Block a user