# Logik Mündlich

## Möglichkeiten um Erfüllbarkeit von Formeln zu überprüfen

### Wahrheitstabelle
- ist eine tabellarische Aufstellung des Wahrheitswertverlaufs einer logischen Aussage

- Die Wahrheitstabelle zeigt für alle möglichen Zuordnungen von endlich vielen (häufig zwei) Wahrheitswerten zu den aussagenlogisch nicht weiter zerlegbaren Teilaussagen, aus denen die Gesamtaussage zusammengesetzt ist, welchen Wahrheitswert die Gesamtaussage unter der jeweiligen Zuordnung annimmt.

- Die Wahrheitstabelle wird genutzt, um Wahrheitswertefunktionen beziehungsweise boolesche Funktionen darzustellen oder zu definieren und um einfache aussagenlogische Nachweise zu führen. Beispielsweise werden Wahrheitstabellen verwendet, um die Bedeutung von Junktoren festzulegen.


### Resolution
#### Wie sieht das Verfahren aus?
- Der Resolutionskalkül ist ein Verfahren um die Unerfüllbarkeit von Formeln in konjunktiver Normalform zu beweisen.
- Der Kalkül enthält nur eine einzige Regel und lässt sich daher sehr einfach implementieren.
- unendlicher Formelmengen erlaubt

- Eine Klausel ist eine endliche Menge von Literalen.

- 
- Eine Resolutionswiderlegung einer Klauselmenge C ist eine Resolutionsableitung der leeren Klause.
- 

#### Korrektheit und Vollständigkeit
- Korrektheit: Wenn eine Menge C von Klauseln eine Resolutionswiderlegung hat, ist C unerfüllbar.
- Vollständigkeit: Jede unerfüllbare Klauselmenge C hat eine Resolutionswiderlegung.
- Beweiss durch Induktion der Korrektheit und Vollständigkeit des Resolutionskalkül: https://isis.tu-berlin.de/pluginfile.php/1793528/mod_resource/content/1/w4l4.pdf

#### Wie ist eine Resolvente definiert?
- 
#### Wann terminiert das Verfahren, aka wann wissen wir, ob eine Formel erfüllbar ist oder nicht?
- Wenn man ein Resolutionswiderlegung draus bekommt. D.h die Formel unerfüllbar ist.
### DPLL-Algorithmen
- DPLL Algorithmen kann eine Belegung ß (wenn ß existiert), die die KNF erfüllt, zurückgeben, damit ist DPLL auch ein Verfahren, um Erfüllbarkeit einer AL Formel zu beweissen.
-
-

### Sequenzenkalkül

#### Wie sieht das Verfahren aus?
- Der Sequenzenkalkül formalisiert die Art, in der wir aus Aussagen neue Folgerungen ableiten.
- Beweis Methode:

#### Wie ist eine Sequenz definiert?

#### Korrektheit und Vollständigkeit
- Korrektheit: Nur gültige Sequenzen können im Sequenzenkalkül hergeleitet werden.
- Vollständigkeit: Alle gültigen Sequenzen können im Sequenzenkalkül hergeleitet werden
#### Wann terminiert das Verfahren, aka wann wissen wir, ob eine Formel erfüllbar ist oder nicht?
- Das Verfahren terminiert,wenn eine gültige Sequenze hergeleitet werden kann.

!!! Eine Sequenz ist gültig, wenn jede Belegung, die alle Formeln in Vorraussetzungen erfüllt, erfüllt die Belegung auch eine Formel in Koklusionen

- Eigenschaften von Sequenzen:

---

## Definierbarkeit
Sätze und freie/gebundene Variablen -> Modellklassen -> FO-axiomatisiertbar -> endlich axiomatisiertbar bzw. definietbar -> m-Äquivalenz -> EF-Spiele und Kompaktheitsatz für FO
### Sätze und freie/gebundene Variablen
- Eine Formel $\varphi$ mit frei($\varphi$) = 0 heißt ein Satz.
- Eine Variable, die in $\varphi$ vorkommt, aber nicht frei ist, heißt gebundene Varibale.
- Eine Formel $\varphi$(x) sagt etwas über Element x innerhalb einer Struktur aus.
- in einer Formel sind die Elementen, die in fester Sturktur A sind und die Formel erfüllen, interessant.
- zB: $\varphi$(A) = {Elementen in A, die Formel phi erfüllen würden}
- Eine Satz $\psi$ sagt etwas über die Struktur insgesamt aus.
- Bei einem Satz sind die Sturkturen, die die Eingentschaft, die in $\psi$ definiert wurde, interessant.
### Beispiel mit Graph und Formel (Bedeutung, Geltungsbereich)

graph LR
    e1 --> e2;
    e2 --> e1;
    e2 --> e3;
    e3 --> e1;

- Seien:
- $\sigma = \{E\}$ eine Graph-Signatur, wobei E ist ein 2-stelliges Relationssymbol.
- $\mathcal A$ ist eine $\sigma$-Sturktur mit Universum $A = \{e1,e2,e3\}$.
- Formel mit gebundene Variablen $\varphi(x):= \exists y\exists zE(x,y)\land E(x,z)$ sagt über Element $x$ aus, dass es 2 Kanten, die von $x$ ausgehen, gibt, sodass $\varphi(\mathcal A)= \{e2\}$
- Ein Satz $\psi :=\forall x\exists yE(x,y), frei(\psi) =\oslash$ sagt über die Struktur aus, dass aus jeden Knoten des Graphs eine Kanter ausgeht.
### Was kann nicht ausgedrückt werden?
### Modellklassen
- Seien $\sigma$ eine Signatur und $\Phi \subseteq FO[\sigma]$ eine Menge von $\sigma$-Sätzen. Die Modellklasse $Mod(\Phi)$ von $\Phi$ ist de Klasse alle $\sigma$-Strukturen A, die $\Phi$ erfüllen.
- Notation: $Mod(\varphi)$ wenn $\Phi$ nur einen Satz enthält.

### Axiomensysteme und Definierbarkeit
- D.h Definierbar wenn die menge $\Phi \subseteq FO[\sigma]$ endlich bzw nur ein Satz enthält.
- Wenn die Konjunktion der alle Formel, die die Eingentschaften von der Struktur darstellen, zu einem Satz äquivalent, dann ist die Struktur diefinierbar.
- 2 Methoden: Kompaktheitssatz und EF-Spiele/m-Äquivalenz

### Quantorenrang

### m-Äquivalenz
- Definition:
- Lema
- m-Äquivalenz und Elementar Äquivalenz

### Resolutions Beweis