# 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