4.9 KiB
4.9 KiB
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.