From 55f259fe881c57d894f33945c28fbe3e0987ed7b Mon Sep 17 00:00:00 2001 From: raj_mathe Date: Sat, 19 Jun 2021 09:49:18 +0200 Subject: [PATCH] =?UTF-8?q?master=20>=20master:=20glossar=20-=20referenzen?= =?UTF-8?q?=20korrigiert,=20=F0=9D=92=9C=20entfernt?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- notes/glossar.md | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/notes/glossar.md b/notes/glossar.md index 8bf5358..ee5835c 100644 --- a/notes/glossar.md +++ b/notes/glossar.md @@ -23,37 +23,37 @@ | `=` | — | `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 | -| `𝒜` | ??? | (nicht verifiziert) Menge der Atome in AL | +| ~~`𝒜`~~ | — | (Eintrag ignorieren—kommt in VL nicht vor!) ~~Menge der Atome in AL~~ | | 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, VL9, Seite 28 | äqv. Formel, Variablensubstitution, so dass jede Var nur gebunden od. frei vorkommt | -| `𝔠` | §88+§89 Definition, VL10, Seiten 55+60 | (Fraktur c) die Herbrand-Konstante („out of bounds“) | +| 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 15 | alle Variablen, Konstanten, Fktsymbole in Term `t` | +| `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, VL9, Seite 21 | Menge gebundener Variablen in `F`| -| `H,H(F)` | §88 Definition, VL10, Seite 55 | Herbrand-Symbole, Herbrand-Universum | -| 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 | +| `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), VL9, Seite 12 | Negationsnormalform - Negation nur bei Literalen | -| PNF | §78 Definition, VL9, Seite 41 | Pränexnormalform - Kette von Quantoren um einen Q-freien Teil | +| 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 7 | äqv. Formel, in der alle Existenzquantoren eliminiert wurden | -| strukturelle Ind | | allgemeine Induktion über die Teilformelbeziehung | -| strukturelle Rek | | rekursive Konstruktionschemata über die Teilformelbeziehung | -| `Sym(F)` | §64 Definition, VL9, Seite 17 | alle „relevanten“ Symbole in `F`: alle **freien** Vars, alle Konstanten, Fktsymbole, Relnsymbole | +| 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) | @@ -66,4 +66,4 @@ ... (wird fortgesetzt) -**ACHTUNG:** Seitennummer können abweichen. +**ACHTUNG:** Seitennr können abweichen.