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
• Funktionssymbole 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