From 23a8ba3a4961fb00ae5cc1fabf59b25dadee7402 Mon Sep 17 00:00:00 2001
From: raj_mathe <raj.dahya@math.uni-leipzig.de>
Date: Sun, 20 Jun 2021 18:35:40 +0200
Subject: [PATCH] master > master: Glossar

---
 notes/glossar.md | 69 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 notes/glossar.md

diff --git a/notes/glossar.md b/notes/glossar.md
new file mode 100644
index 0000000..59632bc
--- /dev/null
+++ b/notes/glossar.md
@@ -0,0 +1,69 @@
+<style>
+    table tbody tr td {
+        vertical-align: top;
+    }
+    table tbody tr td:nth-child(1) {
+        font-size: 10pt;
+    }
+    table tbody tr td:nth-child(2), table tbody tr td:nth-child(3) {
+        font-size: 8pt;
+    }
+</style>
+
+# Glossar #
+
+| Symbol | Referenz (im Skript) | Kurze Beschreibung |
+| :----- | :------------------- | :----------------- |
+| `¬` | §8 Definition, VL2, Seite 8 | Negationsjunktor („nicht“) |
+| `⋀` | §8 Definition, VL2, Seite 8 | Konjunktionsjunktor („und“) |
+| `⋁` | §8 Definition, VL2, Seite 8 | Disunktionsjunktor („oder“) |
+| `⟶` | VL2, Seite 47 | **Abkürzung** für Implikation |
+| `⟷` | VL2, Seite 47 | **Abkürzung** für Doppeltimplikation |
+| `⊨` | §9 Definition, VL2, Seite 34 | Erfüllbarkeitsbeziehung: `I ⊨ F` gdw. `I` erf. `F` |
+| `=` | — | `F = G` gdw. `F` und `G` _dieselbe_ Formel sind |
+| `≡` | §13 Definition, VL3, Seite 11 | `F ≡ G` gdw. `F`, `G` **semantisch** äquivalent |
+| `{...}_⋀` | §39 Definition, VL5, Seite 108 | Mengendarstellung von Disjunktionsglied |
+| ~~-`𝒜`-~~ | — | (**Eintrag ignorieren**: kommt in VL nicht vor!) |
+| AL | (VL2–VL6) | Aussagenlogik |
+| `Aᵢ` | §8 Definition, VL2, Seite 8 | das _i_-te Atom in der AL-Sprache |
+| `Atome(·)` | §5 Definition, V2, Seite 14 | `Atome(F) =` Menge aller Atome in `F` |
+| bereinigt | §76 Definition, VL10, Seite 21 | äqv. Formel, Variablensubstitution, so dass jede Var nur gebunden od. frei vorkommt |
+| `𝔠` | §88+§89 Definition, VL11, Seiten 9+14 | (Fraktur c) die Herbrand-Konstante („out of bounds“) |
+| DNF | §22 Definition, VL3, Seite 55 | disjunktive Normalform für AL und PL |
+| erfüllbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+| `eval(·,·)` | §16 Algorithmus, VL3, Seite 30 | Evaluation: `eval(F,I)=1` gdw. `I ⊨ F` |
+| `ℱ` | §8 Definition, VL2, Seite 8 | Die „AL-Sprache“, Menge aller AL-Formeln |
+| `Fun(t)` | §63 Definition, VL9, Seite 18 | alle Variablen, Konstanten, Fktsymbole in Term `t` |
+| `FV(F)` | §57 Definition, VL8, Seite 27 | Menge freier Variablen in `F` (für Terme siehe `var(t)`) |
+| `g`, `g´`, `g´´`, ... | | Skolemisierung: ∃-Eliminierung mittels Funktionen, die Abhängigkeiten ausdrücken |
+| `GV(F)` | §75 Definition, VL10, Seite 17 | Menge gebundener Variablen in `F`|
+| `H,H(F)` | §88 Definition, VL11, Seite 9 | Herbrand-Symbole, Herbrand-Universum |
+| Herbrand-Interpretation | §89 Definition, VL11, Seite 14 | Interpretation für ein Herbrand-Modell. Alle H-M haben die gleiche Interpretationen von Termen. Nur Relationen können anders interpretiert werden. |
+| KNF | §22 Definition (AL), VL3, Seite 55; §85 Definition (PL), VL10, Seite 89 | konjunktive Normalform für AL und PL |
+| `ℒ` | §8 Definition, VL2, Seite 8 | Die Menge der Literale |
+| PL | (ab VL7) | Prädikatenlogik |
+| NNF | §18 Definition (AL), VL3, Seite 39; §73 Definition (PL), VL10, Seite 8 | Negationsnormalform - Negation nur bei Literalen |
+| PNF | §78 Definition, VL10, Seite 37 | Pränexnormalform - Kette von Quantoren um einen Q-freien Teil |
+| `ℛ,ℛ⁽ᵏ⁾`| §52 Definition, VL7, Seite 72 | Menge der (`k`-stelligen) Relationssymbole, `k≥0`. |
+| `res(·)` | §41–43 Definition, VL6, Seiten 37–43 | `res(F) =` Menge aller Resolventen aus Disjunktionsgliedern aus `F` |
+| `Res(·)` | §43 Definition, VL6, Seite 43 | `Res(F) = F ∪ res(F)` |
+| `Res⁽ⁿ⁾(·)` | §43 Definition, VL6, Seite 43 | `Res(Res(···Res(F)···))`, _n_ Mal |
+| `Res*(·)` | §43 Definition, VL6, Seite 43 | Resolutionshülle |
+| `𝒮,𝒮⁽ᵏ⁾`| §52 Definition, VL7, Seite 72 | Menge der (`k`-stelligen) Funktionssymbole, `k≥0`. **Beachte:** für `k=0` sind dies die Konstanten! |
+| Skolemform | §81, VL10, Seite 62 | äqv. Formel, in der alle Existenzquantoren eliminiert wurden |
+| strukturelle Ind | §6 Theorem, VL2, Seite 24 | allgemeine Induktion über die Teilformelbeziehung |
+| strukturelle Rek | §4 Theorem, VL2, Seite 12 | rekursive Konstruktionschemata über die Teilformelbeziehung |
+| `Sym(F)` | §64 Definition, VL9, Seite 20 | alle „relevanten“ Symbole in `F`: alle **freien** Vars, alle Konstanten, Fktsymbole, Relnsymbole |
+| `𝒯` | §53 Definition, VL7, Seite 74 | Menge der Terme in PL |
+| tautologisch | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+| `TF(·)` | §35 Definition, VL5, Seite 56 | `TF(F) =` Menge aller Teilformeln in `F` (inkl. `F` selbst) |
+| `tᵥ` | §37 Definition, VL5, Seite 64 | Abbildung, die Teilformeln auf Literale abbildet |
+| `tseiᵥ` | §37 Definition, VL5, Seite 64 | Tseitin-Transformation |
+| unerfüllbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+| `𝒱` | §52 Definition, VL7, Seite 72 | Menge der Variablen in PL |
+| `var(t)` | §55 Definition, VL8, Seite 20 | Menge der Variablen in `t` (für Fml siehe `FV(F)`) |
+| widerlegbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+
+... (wird fortgesetzt)
+
+**ACHTUNG:** Seitennr können abweichen.