# Aussagenlogik
## Äquivalenzen

| Name | Formel | Kürzel |
| ----------------------- |:---------------------------------------------------------- | ------ |
| Negation | $p \iff \neg\neg p$ | NEG |
| Implication | $(p \to q)\iff (\neg p \lor q)$ | IMP |
| Contrapos. | $(p \to q)\iff (\neg q \to \neg p)$ | CTP |
| Shunting | $((p \land q) \to r) \iff ( p \to (\neg q \lor r))$ | SHN |
| deMorgan | $\neg(p \land q) \iff (\neg p \lor \neg q)$ | DEM |
| Distributivity $\land$: | $(p \land (q \lor r)) \iff ((p \land q) \lor (p \land r))$ | DST |
| Distributivity $\lor$: | $(p \lor (q \land r)) \iff ((p \lor q) \land (p \lor r))$ | DST |
| Weakening $\land$: | $(p \land q) \implies p$ | WKN |
| Weakening $\lor$: | $p \implies (p \lor q)$ | WKN |
| | $\neg p \iff (p \to F)$ | PSN |
| | $(F \to p) \iff T$ | EFQ |
| | $(\neg p \land p) \iff F$ | CTR |

### Ersetzung äquvialenter Teilformeln

## Syntax PRL


## Operatoren


## Semantik PRL


### Standard Definition

### $\mathbb{N}_0$-Artihmethik

### Boole'sche Algebra

### Halbringssemantik

### Linguistentrick

## Wahrheit und Erfüllbarkeit PRL

## Formelmenge


## Subjunktion und "Kleiner-Gleich"

## Entailment, Schluss, Implikation, Folgerung


# Tautologien

## Deduktionstheorem




## Beweistechniken
### Direkter Beweis durch Wahrheitstabelle

### Direkter Beweis durch Ableitung/Folgerung

### Direkter Beweis zur Reduktion auf Tatuologie

### Beweis durch Kontraposition

### Wechselseitige Inklusion

### Modus Ponens

## Normalformen
### Operatorenbasis


### Konjunktive/Disjunktive Normalform (KNF/DNF)




### Erfüllbarkeit und Gültigkeit in KNF/DNF
#### KNF

#### DNF

## Resolution






### Anwendung Resolution
$\lbrace A,\lbrace A \to B\rbrace\ |\approx B$
$Formelmenge \space P \ | \approx p$

1. Übeführe P in Klauseform
a) A als Klause $\lbrace A \rbrace$
b) $(A\to B) \iff (\neg A \lor B)$ als Klausel $\lbrace \neg A,B \rbrace$
P erfüllungsäquivalent zu $\lbrace\lbrace A \rbrace,\lbrace\neg A,B \rbrace \rbrace$

2. Zielformel negieren : Betrachte $\neg p = \neg B$
3. Überführe $\neg$ p in Klauselform: $\lbrace\lbrace\neg B\rbrace\rbrace$
4. \*
$P\space |\approx p$ gdw. $P´\cup\lbrace \neg p\rbrace \vdash^*_{RES} \oslash$
> $P\space |\approx p \quad |:NEG$
> $P\space |\approx\neg\neg p \quad |:PSN$
> $P\space |\approx(\neg p \to F)\quad |:DT$
> $P\space \cup (\neg p) |\approx F$
5. Leite aus $P\cup\lbrace p \rbrace$ die leere Klausel ab.

# Prädikatenlogik
## Signatur

### Beispiel
$(\forall x: \exists y: p(x,y) \land ((\forall z: r(z) \lor p(f(x))) \to \neg q(c, 7, z)))$

| Name | Schreibweise | Def. |
| ---------- | ----------------------------------------------- | ---- |
| Sorte | s |$Srt_\Sigma = \lbrace s_i \parallel i \in k \rbrace$ |
| Variabeln | s x, y, z |$Var^{(s)}_\Sigma$ |
| Konstanten | $7: \to s \quad$ $c:\to s$ |$c⁰: \to s \in Fnc_\Sigma$ sind $Con^s_\Sigma$ |
| Funktionen | $f:s \to s$ |$Fnc_\Sigma = \lbrace f^{n_j}_j: s_{j_1},...,s_{j_n} \to s_j \parallel n_j \in \mathbb{N}_0, j \in n \rbrace$ |
| Prädikate | $p:s,s \quad$ $r:s \quad$ $p:s \quad$ $q:s,s,s$ |$Prd_\Sigma = \lbrace p^{n_i}_i: s_{i_1},...,s_{i_n} \parallel n_i \in \mathbb{N}_0, i \in m \rbrace$ |

## Grundterm

Funktionen, Konstanten und Funktionen * Konstanten

### Beispiel
$(\forall x: \exists y: p(x,y) \land ((\forall z: r(z) \lor p(f(c))) \to \neg q(c, 7, f(z))))$

$Gnd^s_\Sigma = \begin{Bmatrix}
7 \\
c \\
f(c) \\
\end{Bmatrix}$

## Variablen

## $\Sigma-Terme$

### Beispiel
$(\forall x: \exists y: p(x,y) \land ((\forall z: r(z) \lor p(f(c))) \to \neg q(c, 7, f(z))))$

$Ter_\Sigma = Gnd_\Sigma \cup
\begin{Bmatrix}
x \\
y \\
z \\
f(z)
\end{Bmatrix}$

## Prädikate


### Skopus

## Variablen
* In $p$ nicht gebundene Variabeln heißen frei.
* $var(p)$ ist die Menge aller in der Formel $p$ vorkommenden Variabeln.
* $var(t)$ ist die Menge aller in dem Term $t§ vorkommenden Variablen.
* $fvr(p)$ und $bvr(p)$ sind die Teilmengen der frei/gebunden vorkommenden Variabeln.
* p heißt geschlossen, wenn $fvr(p) =\emptyset$
* p heißt bereinigt, wenn $bvr(p) \cap fvr(p) = \emptyset$
* Ein Term (Formel) t (p) heißt Grundterm (Grundformel), wenn er (sie) keine Variabeln beinhaltet $var(t) = \emptyset$ (bzw. $var(p) = \emptyset$)

### Beispiel
$\exists z: \forall y: ((p(z, y) \land q(y,x)) \to (\forall x: p(x,y) \lor p(z, x)))$

$var(p) = \lbrace x, y, z \rbrace$
$bvr(p) = \lbrace x, y, z \rbrace$
$fvr(p) = \lbrace x \rbrace$
bereinigt: nein, weil $bvr(p) \cap fvr(p) \neq \emptyset$

## Substitution


* Tauschen von freien Variabeln zu Termen.
* Seien die Variabeln nach der Subtition gebunden, ist die Subtiution unzulässig.
* Subtitionen wird gleichzeitig ausgeführt.

## Unifikation

## Semantik der FOL
### Beispiel 1

### Beispiel 2

### $\Sigma-Alebgren$

### Variabeln -Auswertung

### Termauswertung

### Semantik der Prädikatenlogik




### Warheit, Erfüllbarkeit, Gültigkeit und Modelle FOL

3 . Modell ist die Gültigkeit unter einer Algebra
4 . Gültigkeit ist das Modell für alle Algebren

#### Beispiele ohne Quantoren
##### Beispiel 1

##### Beispiel 2

#### Beispiele mit Quantoren
##### Beispiel 1

##### Beispiel 2

##### Beispiel 3


## Resolution Prädikatenlogik

1. Bereinigen $fvr(p)\cap bvr(p) = \emptyset \quad[? /?]$
2. Gebundene Umbenennung $\quad p[?/?]$
3. Prenexform $Q x_1: ... Qx_n:MATRIX$
>Matrix ist die Formel nach den Quantoren (Präfix)
4. Universeller Abschluss $\backslash\forall \quad \forall_{n+1}Q_1 ... Q_n$
5. Skolemisierung: $\quad\nexists\quad sk_{\square}(X_1...X_n)$
6. Generalisierunglemma: Allquantoren weglassen$\xcancel{\forall}$
7. p in CNF überführen (Atomare Teile)
8. Menge der Klause bilden
9. Resolution

### Prenex-Form

Alle Quantoren auf die linke Seite.

#### Quantoren-Gesetzte


### Universeller Abschluss

Alle freien Variabelln werden durch All-Quantoren gebunden. Neue Quantoren ganz links von den alten.

### Gebundene Umbennung

Variabeln die gebunden sind, können einfach einen anderen "Namen" zugeordnet werden.

### Bereinigte Formel

1. $fvr(p) \cap bvr(p) = \emptyset$
2. $Q_1x_1 Q_2x_2$ in $p$ ist $x_1 \neq x_2$ (keine mehrfach Quantifizierung)

Formeln können durch Substition und gebundene Umbennung bereinigt werden.

### Skolemisierung

Ersetzung der Existenzquantoren mit Funktionen ($sk_y(x_1,...x_n)$). y ist die Variable den der Existenzquantor bindet und x sind die von den Allquantoren gebundene Variablen, von dem der Existenzquantor abhängt.

#### Beispiel Skolemisierung
$\exists y_1: \forall x_1: \forall x_2: \exists y_2:p(x_1, y_2, y_1, x_2)$
$[y_1 / sk_{y_1}, y_2 / sk_{y_2}(x_1, x_2)]$
$\forall x_1: \forall x_2:p(x_1, sk_{y_2}(x_1, x_2), sk_{y_1}, x_2)$

### Skolemnormalform

# Sequenzkalkül







# Natürliche Deduktion










# Beispiele
## Übung 1




## Übung 2







## Übung 3












## Übung 4







## Übung 5




## Übung 6








## Übung 7










## Übung 8







## Übung 9





## Übung 10





## Aussagenlogik
### Semantik, Erfüllbarkeit
#### Beweisen Sie: Für eine endliche Menge P von PRL-Formel gilt $Sat(P) \subseteq Sat(\bigvee P)$.

Sei P endliche Menge von PRL | $Sat(P) \subseteq Sat(\bigvee P)$
Annahme: $P \subseteq \lbrace A, B, C \rbrace |\approx Sat(P) \subseteq Sat(\bigvee P)$
$Sat(\bigvee P) = min(\lbrace I^\alpha_{\mathbb{N}_0} \cdot A, I^\alpha_{\mathbb{N}_0} \cdot B, I^\alpha_{\mathbb{N}_0} \cdot C \rbrace)$
Dadurch gilt das $Sat(P)$ auch immer $Sat(\bigvee P)$ erfüllt und damit $Sat(P) \subseteq Sat(\bigvee P)$ gültig ist.

#### Sei $p \in Fml_{PRL}$. Zeigen Sie: $(F \to p)$ ist (allgemein-) gültig.
$I^\alpha_{\mathbb{N}_0} \cdot (F \to p) = max(\lbrace 1 - I^\alpha_{\mathbb{N}_0} F, I^\alpha_{\mathbb{N}_0} p \rbrace)=max(\lbrace1-0, p' \rbrace) = max(\lbrace 1, p' \rbrace) = 1$

#### Sei $A \in Prp$. Zeigen Sie: $(A \to F)$ ist nicht (allgemein-) gültig.
$I^\alpha_{\mathbb{N}_0} \cdot (A \to F) = max(\lbrace 1 - I^\alpha_{\mathbb{N}_0} A, I^\alpha_{\mathbb{N}_0} F \rbrace)=max(\lbrace1- \alpha(A), 0 \rbrace) = max(\lbrace 1 - 1, 0 \rbrace) = 0$

#### Beweisen oder wiederlegen der Aussagen.
##### $\lbrace \neg p, (q \land r)\rbrace |\approx (p \to r)$
$\iff \lbrace \neg p, (q \land r), p\rbrace |\approx r$
$\iff I^\alpha \vDash \lbrace \neg p, (q \land r), p \rbrace \implies I^\alpha \vDash r$
Es gibt keine Interpretation, die sowohl $\neg p$ und $p$ wahr macht.
(Resolution möglich)

# Index
## Theoreme
### Aussagenlogik
Thm.1: Alle Semantiken sind Isomorph S.25
Thm.2-7: Ersetzung äquivalenter Teilformen S.38
Thm.8: F ist unerfüllbar S.42
Thm.9: Ex falso sequitur quodlibet S.42
Thm.10: Das Deduktionstheorem für PRL (1 / 2) S.44
Thm.11: Das Deduktionstheorem für PRL (2 / 2) S.45
Thm.12: Negation und Äquivalenz S.50
Thm.13: Dualität S.50
Thm.14: Tautologien S.51
Thm.15: Äquivalenzen und Umformungsregeln S.52+
Thm.16: Subjunktion und Implikation S.54
Thm.17: Kontraposition S.61
Thm.18: Kompaktheitstheorem S.63
Thm.19: {↑} ist eine minimale Operatorbasis S.65
Thm.20: Existenz von Normalformen S.70
Thm.21: Hinweis auf Resolution S.73
Thm.22: ND ist Korrekt bzgl.PRL S.83
Thm.23: Resolutionslemma S.105
Thm.24: Widerlegungsbeweise in $RES_{PRL}$ mit $Res^*$ S.108
Thm.25: $RES_{PRL}$ als Widerlegungskalkül S.110

### Prädikatenlogik
Thm.26: Rechnen mit Substitutionen S. 139
Thm.27: Substitutionslemma für Terme $Ter_{\Sigma}$ in FOL S.153
Thm.28: Koinzidenzlemma für $Ter_{\Sigma}$ in FOL S.153
Thm.29: Koinzidenzlemma FOL S.157
Thm.30: Tautologien S.166
Thm.31: Quantorengesetze S.183
Thm.(ctd): Quantorengesetze S.186
Thm.32: Generalisierungslemma S.189
Thm. 33: Prenex-Äquivalenz S. 190
Thm. 34: PCNF-Äquivalenz. S. 191
Thm. 35: Syntax und Semantik von Grundliteralmengen S. 200
Thm. 36: Skolemtheorem S. 201
Thm. 37: Kompaktheitstheorem S. 201
Thm. 38: Unifikationsalgorithmus S. 203
Thm. 39: Erfüllbarkeitsbeweis S. 206
Thm. 40: RES ist deduktiv korrekt S. 209
Thm. 41: RES als Widerlegungskalkül ist korrekt S. 209
Thm. 42: RES als Widerlegungskalkül ist vollständig S. 209
Thm. 43: Grundlagen der SLD Widerlegung S. 216

## Definitionen
### Aussagenlogik
Def.1: Logik S.6
Def.2: Proposition S.15
Def.3: Wahrheitswerte S.15
Def.4: Propositionale Formeln S.16
Def.5: Interpretation S.18
Def.6: Belegung und Wahrheitswertzuweisung S.19
Def.7: Wahrheitstabellen für die PRL-Operator Semantik S.20
Def.8: PRL-Semantik via BA S.21
Def.9: PRL-Semantik in $\mathbb{N}_0$-Arithmetik S.22
Def.10: PRL-Semantik via Halbring S.23
Def.11: Eine Abstrakte Definition S.29
Def.12: Erfüllbarkeit und Modelle S.31
Def.13: Implikation und Äquivalenz S.32
Def.14: Schlussfolgerung, (logisches)"Schliessen" S.40
Def.15: Allgemeingültigkeit von Tautologien S.41
Def.16: Punktweise Funktionsänderung S.49
Def.17: Operatorbasis S.65
Def.18: Konjunktive / Disjunktive Normalformen (KNF/DNF) S.68
Def.19: Klausel S.69
Def.20: Ein vollst./korr. Kalkül für gültige Aussagen S.75
Def.21: ND 1/3 Strukturelle Regeln S.80
Def.22: ND 2/3 Logische Prinzipien S.85
Def.23: ND 3a/3: Schlussregeln S.86
Def.24: ND 3b/3: Implikationseinführung ("Annahme") S.87
Def.25: Korrektheit von ND 3/3 S.88
Def.26: Sequenz S.98
Def.27: Gültigkeit von Sequenzen S.98
Def.28: $RES_{PRL}$ S.104
Def.29: Resolutionsoperation S.107
### Prädikatenlogik
Def.30: Signatur S.130
Def.31: $\Sigma$-Grundterme S.132
Def.32: $\Sigma$-Terma S.133
Def.33: ($\Sigma$-) Prädikate
Def.34: Die Sprache der Prädikatenlogik, $Fml_{\Sigma}$ S.135
Def.35: Vorkommen von Variablen S.137
Def.36: $\Sigma$-Substitution S.138
Def.37: Zulässigkeit von Substitutionen S.139
Def.38: Komposition von Substitutionen S.139
Def.39: Varianten von Substitutionen S.140
Def.40: Umbennung S.140
Def.41: Varianten S.140
Def.42: Unifikator S.141
Def.43: Allgemeinste Unifikatoren S.141
Def.44: $\Sigma$-Algebra
Def.45: (Variablen-) Belegung in FOL S.152
Def.46: Auswertung von $\Sigma$-Termen S.153
Def.47: Semantik von FOL-Formeln S.155
Def.(ctd): Semantik von FOL-Formeln S.156
Def.48: Wahrheit, Erfüllbarkeit, Gültigkeit und Modelle S.159
Def.49: Implikation und Äquivalenz, Entailment S.165
Def.50: Modellklassen, Theorien, Axiomensysteme S.174
Def.51: Herbrand Algebren S.178
Def.52: Prenex-Form S.183
Def.53: Bereinigte Formeln S.190
Def.54: Skolemisierung S.193
Def.55: Skolemnormalform S.19
Def.56: Grundinstanzen S.199
Def.57: Unifikatoren, Unifikation, MGU S.203
Def.58: Die Resolutionsregel S.205
Def.59: Hornklauseln S.215
Def.60: PRL / FOL-Sequenzen S.224
Def.61: Gültigkeitsbegriff für Sequenzen S.225
Def.62: LK-Axiom S.227
Def.63: LK-Strukturregeln S.228
Def.64: LK-Junktorregeln S.231
Def.65: LK-Junktorregeln (b) S.235
Def.66: LK-Quantorenregeln S.237