logik2021/notes/glossar.md

58 lines
3.6 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<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 | 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 |
| AL | (VL2VL6) | 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, sodass jede Var nur gebunden od. frei vorkommt |
| `𝔠` | §88+§89 Definition, VL10, Seiten 55+60 | (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 |
| `g`, `g´`, `g´´`, ... | | Skolemisierung: ∃-Eliminierung mittels Funktionen, die Abhängigkeiten ausdrücken |
| `H,H(F)` | §88 Definition, VL10, Seite 55 | Herbrand-Symbole, Herbrand-Universum |
| Herbrand-Struktur | | `` |
| 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 |
| 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 |
| `res(·)` | §4143 Definition, VL6, Seiten 3743 | `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 |
| 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 |
| 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 |
| widerlegbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
... (wird fortgesetzt)