master > master: protokoll woche10

notes/glossar.md

@@ -23,16 +23,30 @@
 | `=` | — | `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 | (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, 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(·)` | §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 |
+| 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 |

protocol/README.md

@@ -10,8 +10,8 @@ Inhaltsverzeichnis
 - [Vorlesungswoche 6](./woche6.md) HA Blatt 1; [Zoom Aufzeichnung](https://t1p.de/m431).
 - [Vorlesungswoche 7](./woche7.md) (_keine Übung: ...Pfingsten..._)
 - [Vorlesungswoche 8](./woche8.md) Semaufg Blatt 3; [Zoom Aufzeichnung](https://t1p.de/fmok).
-- [Vorlesungswoche 9](./woche9.md) HA Blatt 2; [Zoom Aufzeichnung](https://t1p.de/8vmh). **⟵ wir sind hier**
+- [Vorlesungswoche 9](./woche9.md) HA Blatt 2; [Zoom Aufzeichnung](https://t1p.de/8vmh).
-- [Vorlesungswoche 10](./woche10.md) Semaufg Blatt 4; [Zoom Aufzeichnung].
+- **[Vorlesungswoche 10](./woche10.md) Semaufg Blatt 4; [Zoom Aufzeichnung]. ⟵ _wir sind hier_**
 - [Vorlesungswoche 11](./woche11.md) HA Blatt 3; [Zoom Aufzeichnung].
 - [Vorlesungswoche 12](./woche12.md) Semaufg Blatt 5; [Zoom Aufzeichnung].
 - [Vorlesungswoche 13](./woche13.md) HA Blatt 4; [Zoom Aufzeichnung].

protocol/woche10.md

@@ -7,6 +7,9 @@
     - [ ] SemA 4.1
     - [ ] SemA 4.2
     - [ ] SemA 4.3
+    - [ ] SemA 4.4
+    - [ ] SemA 4.5
+    - Anmerkungen zu HA
 - [ ] restliche Zeit für allg. Fragen
 
 ## Nächste Woche ##