diff --git a/notes/glossar.md b/notes/glossar.md index 3b7a137..15f7511 100644 --- a/notes/glossar.md +++ b/notes/glossar.md @@ -32,9 +32,11 @@ | 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 | +| `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, VL9, Seite 21 | Menge gebundener Variablen in `F`| | `H,H(F)` | §88 Definition, VL10, Seite 55 | Herbrand-Symbole, Herbrand-Universum | -| Herbrand-Struktur | | `` | +| Herbrand-Interpretation | §89 Definition, VL10, Seite 60 | 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 20 | konjunktive Normalform für AL und PL | | `ℒ` | §8 Definition, VL2, Seite 8 | Die Menge der Literale | | PL | (ab VL7) | Prädikatenlogik | @@ -52,6 +54,7 @@ | `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 | +| `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)