40 lines
2.1 KiB
Markdown
40 lines
2.1 KiB
Markdown
<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 | 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.,<br>widerlegbar,<br>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` selbst) |
|
||
| `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)
|