# Glossar # | Symbol | Referenz (im Skript) | Kurze Beschreibung | | :----- | :------------------- | :----------------- | | ℒ | §8 Definition, VL2, Seite 8 | Die Menge der Literale | | ℱ | §8 Definition, VL2, Seite 8 | Die „AL-Sprache“, Menge aller AL-Formeln | | Aᵢ | §8 Definition, VL2, Seite 8 | das i-te Atom in der AL-Sprache | | ¬ | §8 Definition, VL2, Seite 8 | Negationsjunktor („nicht“) | | ⋀ | §8 Definition, VL2, Seite 8 | Konjunktionsjunktor („und“) | | ⋁ | §8 Definition, VL2, Seite 8 | Konjunktionsjunktor („oder“) | | ⟶ | VL2, Seite 47 | **Abkürzung** für Implikation | | ⟷ | VL2, Seite 47 | **Abkürzung** für Doppeltimplikation | | erf., taut.,
widerlegbar,
unerf. | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme | | ⊨ | §9 Definition, VL2, Seite 34 | Erfüllbarkeitsbeziehung: I ⊨ F gdw. I erf. F | | ≡ | §13 Definition, VL3, Seite 11 | F ≡ G gdw. F, G **semantisch** äquivalent | | = | — | F = G gdw. F und G _dieselbe_ Formel sind | | eval(·,·) | §16 Algorithmus, VL3, Seite 30 | Evaluation: eval(F,I)=1 gdw. I ⊨ F | | Atome(·) | §5 Definition, V2, Seite 14 | Atome(F) = Menge aller Atome in F | | TF(·) | §35 Definition, VL5, Seite 56 | TF(F) = Menge aller Teilformeln in F (inkl. F) | | tᵥ | §37 Definition, VL5, Seite 64 | Abbildung, die Teilformeln auf Literale abbildet | | tseiᵥ | §37 Definition, VL5, Seite 64 | Tseitin-Transformation | | 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 | ... (wird fortgesetzt)