Behandelter Stoff
Folien
Folien- satz |
Inhalt |
---|---|
01 | Organisatorisches |
02 | Aussagenlogik: Modellierung von Sudoku; 8-Damen-Problem; Allgemeine Syntax und Semantik sowie Grundbegriffe, Tautologien und Sätze; Basis; Erfüllbarkeit; Allgemeingültigkeit; $M \models A$ |
03 | Aussagenlogik: Craig-Interpolation |
04 | Aussagenlogik: Normalformen (KNF, DNF, KKNF) |
05 | Binary Decision Diagrams: (normierte) Shannon-Formeln, sh-Operator, Shannon-Graph, Reduzierte Shannon-Graphen |
06 | SAT; Satz von Cook; Horn-Formeln; DPLL |
07 | Prädikatenlogik: Syntax (PL1); JML; (Kollisionsfreie) Substitutionen; Unifikation und der Algorithmus von Robinson; Unifikationstheorem |
08 | Pradikatenlogik: Semantik; Interpretation; Koinzidenzlemma; Substitutionslemma für Terme (und das für Formeln); Hoare-Kalkül; Modell; (Logische) Folgerung; Allgemeingültigkeit; Folgerbarkeit |
09 | Pradikatenlogik: Normalformen; Negationsnormalform; Pränexe Normalform; Skolem-Normalform; Herbrand-Strukturen; Satz von Herbrand; Endlichkeitssatz der Aussagenlogik |
10 | Beweistheorie (Einführung) |
11 | Hilbertkalkül; Deduktionstheorem; Vollständigkeit der PL1; Kompaktheitssatz; Endlichkeitssatz |
12 | Aussagenlogik: Resolutionskalkül; 1-Resolution |
13 | Prädikatenlogik: Resolutionskalkül |
14 | Tableaukalkül |
19 | Prädikatenlogik: Sequenzenkalkül |
21 | Peano-Arithmetik; Unentscheidbarkeit |
28 | JML |
22 | Reduktionssysteme: Gleichungslogik; Satz von Birkhoff; Termersetzungssysteme; Reduktionssysteme; Kanonische Reduktionssysteme; Noethersche Induktion; (lokale) Konfluenz |
23 | Termersetzungssysteme; Kritische Paare |
27 | Modallogik; Bakery-Algorithmus; Kripke-Strukturen; Charakterisierungstheorie; Entscheidbarkeit modaler Logiken |
41 | (Vollständige) endliche Automaten; NEAs; Spontane Übergänge; Satz von Myhill und Büchi (vgl. Konstruktion); Reguläre Ausdrücke |
42 | Büchi-Automaten; Zerlegungssatz |
43 | Lineare Temporale Logik; omega-Struktur; LTL-Formeln; LTL-Semantik; |
45 | LTL und Büchi-Automaten |
50 | Wiederholung |
Übungsblätter
Übungsblatt | Lsg | Inhalt |
---|---|---|
ÜB 1: Aussagenlogik | Lsg | Erfüllbarkeit, Unerfüllbarkeit, Allgemeingültigkeit, Tautologie, KNF, DNF, Interpolanten |
ÜB 2: Aussagenlogik | Lsg | KKNF, BDD, Shannon Graphen |
ÜB 3: Aussagenlogik, PL1 | Lsg | DNF, KNF, DPLL |
ÜB 4: PL1 | Lsg | PL1 (Variante des Zebrarätsels); Unifikation |
ÜB 5: PL1 | Lsg | Verwandschaftsbeziehungen; (Java) Integer; Interpretation/Modell/Formel; Erfüllbar / allgemeingültig / unerfüllbar |
ÜB 6: PL1 | Lsg | Pränexnormalform; Skolemnormalform (09) |
ÜB 7: PL1, Aussagenlogik | Lsg | Hilbertkalkül (11); Resolutionskalkül (12) |
ÜB 8: PL1 | Lsg | Resolutionskalkül, Tableaukalkül (13, 14) |
ÜB 9: PL1, Aussagenlogik | Lsg | Resolutionskalkül, Sequenzenkalkül (19) |
ÜB 10: JML | Lsg | Klassen-Invarianten; Methoden-Vertrag; Spezifikation |
ÜB 11: Reduktionssysteme | Lsg | reflexive, transitive Hülle; (lokal) konfluent; noetersch; irreduzibel; Ackermann-Funktion; noethersche Induktion (22) |
ÜB 12: Modallogik | Lsg | Kripke-Strukturen (27) |
ÜB 13: Büchi-Automaten | Lsg | $\omega$-Sprachen, $\omega$-reguläre Ausdrücke (41, 42) |
ÜB 14: LTL | Lsg | LTL-Formeln und Büchi-Automaten (43, 45) |
JML
Ein paar Auszüge aus den Folien von Prof. Dr. Beckert. Ich finde daran sieht man schön, wie JML funktioniert:
public class PostInc{
public PostInc rec;
public int x, y;
/*@ public invariant x >= 0 && y >= 0 &&
@ rec.x >= 0 && rec.y >= 0;
@*/
/*@ public normal_behavior
@ requires true;
@ ensures rec.x == \old(rec.y) &&
@ rec.y == \old(rec.y) + 1;
@*/
public void postinc() {
rec.x = rec.y++;
}
}
Quelle: 28JML.pdf#page=3
Wichtig ist noch:
/*@
@ assignable \nothing;
@ ensures (\forall int j; l <= j && j < \result; a1[j] != a2[j] );
@*/
Das assignable \nothing
besagt, dass keine Werte (nach außen sichtbar)
verändert werden dürfen.
Die Schleifen-Syntax ist \forall int i; B; R
, wobei B
eine
Bereichseinschränkung und R
der Schleifenrumpf ist. Es gibt auch noch
\exists int i; B; R
.
Die Prädikatenlogischen Operatoren sind
!
: Negation&&
: und||
: oder==>
: Implikation<==>
: Äquivalenz==
: Gleichheit
public int commonEntry(int l, int r) {
int k = l;
/*@ loop_invariant
@ l <= k && k <= r &&
@ (\forall int i; l<=i && i<k; a1[i] != a2[i]);
@ assignable \nothing;
@ decreases a1.length - k;
@*/
while(k < r) {
if(a1[k] == a2[k]){break;}
k++;
}
return k;
}
Quelle: 28JML.pdf#page=44
Modallogik
Interpretation | $\square A$ bzw. $\square_p A$ | $\diamond A$ |
---|---|---|
A ist notwendigerweise wahr | A ist möglicherweise wahr | |
Zeit | A ist zu jedem zukünfigem Zeitpunkt wahr | Es gibt einen zukünftigen Zeitpunkt zu dem A wahr ist |
Glauben | Ein Agent p glaubt A | A ist konsistent mit den Aussagen, die p für wahr hält |
Wissen | Ein Agent p weiß A | p weiß nicht, dass A falsch ist |
Programmausführung | Nach Ausführung des Programs p gilt A | Es gibt eine Ausführung des Programs p, nach der A wahr ist |
Kurz und Gut
Die folgenden Stichpunkte sollte man (größtenteils nur sinngemäß) auswendig können und verstehen:
- Eine Signatur \(\Sigma\) ist eine abzählbare Menge von Symbolen. Die Elemente der Signatur heißen "Aussagevariablen".
- Eine Interpretation ist eine Abbildung \(I: \Sigma \rightarrow \{W, F\}\)
- Ein Modell einer Formel \(A \in For0_\Sigma\) ist eine Interpretation \(I\) mit
\(val_I(A) = W\).
Ein Modell einer Formel ist also einfach eine Variablenbelegung, welche die Formel erfüllt. - Für \(M \subseteq For0_\Sigma, A \in For0_\Sigma\) gilt: \(M \models A\) (lies: aus M folgt A), falls jede Variablenbelegung, welche \(M\) erfüllt, auch \(A\) erfüllt.
- \(A \rightarrow B \equiv \neg A \lor B\)
- \(A \models B\) gdw. \(\models A \rightarrow B\)
- Der shannon-Operator \(sh(a,b,c)\) ist if(a) {c} else {b}.
- Die Craig-Interpolation von \(A \rightarrow B\) ersetzt alle Aussagevariablen \(\{\text{Aussagevariable } a \in A | a \notin B\}\) mit \(c_i\) (\(i=1,\dots,n\)). Die Interpolante ist dann \(C := \bigvee_{(c_1, \dots, c_n) \in \{0,1\}^n} A[c_1, \dots, c_n]\).
- Eine DNF heißt "vollständig" bzgl. einer Signatur \(\Sigma\), wenn falls für jedes \(P \in \Sigma\) in jeder Klausel entweder \(P\) oder \(\neg P\) vorkommt.
- Eine DNF heißt "minimal", wenn jede kürzere Formel nicht äquivalent ist.
- KKNF-Konstruktion: (1) Shortcuts \(Q_1, \dots, Q_n\) für binäre Operatoren erstellen. Diese Shortcuts dürfen auch andere Shortcuts verwenden (2) Äquivalenzen auflösen (3) In KNF umformen.
- \(sh(P_i, A, B)\) heißt normiert, wenn \(A\) und \(B\) normiert sind und jede in \(A \cup B\) vorkommende Variable \(P_j\) gilt \(i < j\).
- Ein Shannon-Graph heißt reduziert, wenn es keine zwei Knoten \(v,w\) gibt, sodass die beiden in \(v\) und \(w\) verwurzelten Teilbäume isomorph sind und es auch keinen Knoten gibt, bei dem beide ausgehenden Kanten in den selben Nachfolger führen.
- Reduzierter Shannon-Graph = OBDD = BDD = ordered binary decisio diagram
- Bei gegebener Indizierung sind reduzierte Shannon-Graphen bis auf Isomorphie eindeutig. Ist die Indizierung nicht gegeben, macht die Variablenanordnung einen großen Unterschied in der Größe (Knotenmenge) des reduzierten Shannon-Graphen.
- Multiplikation \(k\)-stelliger Binärzahlen: Für jede Ordnung \(<\) der Variablen in \(X=\{x_0, \dots, x_{k-1}, y_0, \dots, y_{k-1}\}\) gibt es einen Index \(0 \leq i < 2k\), sodass der BDD \(B_{Mult_i,<}\) mindestens \(2^{k/8}\) Knoten besitzt.
- Horn-Formel: Formel in KNF, wobei jede Klausel höchstens ein positives Literal enthält.
- Negationsnormalform: Negationen nur vor Atomen.
- Bereinigte Formel: (1) \(Frei(A) \cap Bd(A) = \emptyset\) (2) Die hinter Quantoren stehenden Variablen sind paarweise verschieden.
- Pränexe Normalform: \(A = Q_1 x_1 Q_2 x_2 Q_3 x_3 \dots Q_n x_n B\), wobei \(B\) quantorenfrei sein muss. Dann heißt \(B\) die Matrix von \(A\).
- Die Pränexe Normalform ist nicht eindeutig.
- Skolem-Normalform: (1) geschlossene Formel (2) \(\forall x_1 \dots \forall x_n B\) (3) Matrix \(B\) ist in KNF
- Gödelscher Vollständigkeitssatz: Es gibt einen Kalkül der PL1 derart, dass für jede Formelmenge \(\Gamma\) und für jede Formel \(\varphi\) gilt: \(\varphi\) folgt genau dann aus \(\Gamma\), wenn \(\varphi\) im Kalkül aus \(\Gamma\) hergeleitet werden kann. In Zeichen: \(\Gamma \models \varphi \Leftrightarrow \Gamma \vdash \varphi\).
- Gödelscher Unvollständigkeitssatz:
- Jedes hinreichend mächtige, rekursiv aufzählbare formale System ist entweder widersprüchlich oder unvollständig.
- Jedes hinreichend mächtige konsistente formale System kann die eigene Konsistenz nicht beweisen.
- Kompaktheitssatz: Wenn A aus einer unendlichen Teilmenge der Formelmenge folgt, dann auch aus einer endlichen.
- Endlichkeitssatz: Eine Menge \(M \subseteq For_\Sigma\) hat genau dann ein Modell, wenn jede endliche Teilmenge von \(M\) ein Modell hat.
- Der Resolutionskalkül arbeitet nur mit Formeln in Skolemnormalform.
- Tableau-Kalkül:
- Typ-\(\alpha\): Alles, was keine Quantoren hat und eindeutig ist
- Typ-\(\beta\): Alles, was keine Quantoren hat, aber nicht eindeutig ist
- Typ-\(\gamma\): Unendlich viele
- Typ-\(\delta\): min. eines
- Ob eine prädikatenlogische Formel allgemeingültig ist, ist unentscheidbar.
- Die Menge der allgemeingültigen prädikatenlogischen Formeln ist rekursiv aufzählbar.
- Die Menge der erfüllbaren prädikatenlogischen Formeln ist nicht rekursiv aufzählbar.
- Ein Reduktionssystem ist ein Tupel \((D, \succ)\), wobei \(D \neq \emptyset\) eine Menge ist und \(\succ\) eine Relation auf \(D\) ist.
- \(\rightarrow\) bezeichnet die reflexive, transitive Hülle von \(\succ\).
- \(\stackrel{+}{\rightarrow}\) bezeichnet die transitive Hülle von \(\succ\).
- \(\leftrightarrow\) bezeichnet die reflexive, transtive und symmetrische Hülle von \(\succ\).
- \((D, \succ)\) heißt konfluent \(:\Leftrightarrow \forall s_1, s_2, s_3 \in D\) mit \(s \rightarrow s_1 \land s \rightarrow s_2 \exists t \in D: s_1 \rightarrow t \land s_2 \rightarrow t\)
- \((D, \succ)\) heißt lokal konfluent \(:\Leftrightarrow \forall s_1, s_2, s_3 \in D\) mit \(s \succ s_1 \land s \succ s_2 \exists t \in D: s_1 \rightarrow t \land s_2 \rightarrow t\)
- \((D, \succ)\) heißt noethersch, wenn es keine unendlichen Folgen \(s_0 \succ s_1 \dots \succ s_i \succ \dots\) gibt.
- Ein konfluentes und noethersches Reduktionssystem heißt kanonisch.
- Ein Element \(s \in D\) heißt irreduzibel (oder eine Normalform) in \((D, \succ)\), wenn kein \(t \in D\) existiert mit \(s \succ t\).
- Sei \(s \in D\). Ein Element \(s_0 \in D\) heißt eine Normalform für \(s\) in \((D, \succ)\), wenn \(s_0\) irreduzibel ist und \(s \rightarrow s_0\) gilt.
- In kanonischen Reduktionssystemen hat jedes Element eine eindeutige Normalform.
- \((D, \succ)\) ist noethersch und lokal konfluent \(\Rightarrow (D, \succ)\) ist konfluent.
- Eine Kripke-Struktur ist ein Tupel \(\mathscr{K} = (S, R, I)\) mit
- \(S \neq \emptyset\) ist die Menge der Zustände bzw. der möglichen Welten. \(s \in S\) heißt also auch eine "Welt".
- \(R \subseteq S \times S\) ist die Zugänglichkeitsrelation
- \(I: (\Sigma \times S) \rightarrow \{W, F\}\) ist die Interpretation der Aussagenlogischen Variablen
- \((S, R)\) heißt der Kripke-Rahmen von \(\mathscr{K}\).
- \(\square A \rightarrow A\) ist nur in reflexiven Kripke-Strukturen eine Tautologie.
- Ein endlicher Automat ist ein Tupel \((S, V, \delta, s_0, S_1)\), wobei
- \(S\) eine endliche Zustandsmenge ist,
- \(V\) ein endliches Alphabet (terminale Zeichen) ist,
- \(\delta: S \times V \rightarrow S\) eine Funktion ist, die besagt bei welchem Eingabezeichen man von welchem Zustand aus in welchen Zustand kommt,
- \(s_0 \in S\) ein Startzustand und
- \(S_1 \subseteq S\) die Menge der Endzustände ist
- \(V^\omega\) ist die Menge der unendlichen Wörter mit Buchstaben aus \(V\).
- \(w(n)\) ist der \(n\)-te Buchstabe des Wortes \(w\).
- \(w \downarrow (n)\) ist das endliche Anfangsstück \(w(0)\dots w(n)\) von \(w\).
- \(\varepsilon \notin V^\omega\)
- Für \(K \in V^*\) und \(J \in V^\omega\) ist \(KJ=\{w_1 w_2 | w_1 \in K, w_2 \in J\}\)
- Für \(K \in V^*\) ist \(\overset{\rightarrow}{K}=\{w \in V^\omega | w \downarrow (n) \in K \text{ für unendlich viele } n\}\)
- Ein Büchi-Automat ist ein nicht deterministischer endlicher Automat, der Wörter akzeptiert, wenn es eine Berechnungsfolge mit unendlich vielen Finalzuständen gibt. (vgl. Beispiel)
- A U B: A gilt, bis B gilt (das U steht für "until"). Allerdings gilt B auch irgendwann. Es kann also nicht sein, dass A unendlich lange gilt und B nie.
- \(A\;\textbf{U}_W\;B\) bedeutet, dass entweder immer A und gleichzeitig nie B gilt, oder dass irgendwann B gilt und davor gilt immer A. Das 'W' steht für 'weak'.
- \(A\;\textbf{V}\;B\): B gilt so lange, bis A gilt. Daher wird V auch 'Release-Operator' genannt.
- \(\diamond \square P\): Es gibt einen Zeitpunkt, ab dem immer B gilt.
- Zu jeder LTL-Formel gibt es einen effektv konstruierbaren Büchi-Automaten.
- Erfüllbarkeit und Allgmeingültigkeit von LTL-Formeln ist entscheidbar.
- Ein Kalkül ist korrekt, wenn alles was formal ableitbar auch wahr ist. (vgl. Korrektheit (Logik))
- 08Pk1Semantik-print.pdf, Folie 34/37: QxB steht für "Quantor x B", wobei der Quantor entweder \(\exists\) oder \(\forall\) ist, \(x\) eine Variable ist und \(B\) eine Formel ist.
Wissens-Check
Folgende Fragen sollte man für die Klausur schnell beantworten können:
- Nenne 3 Basen für die Aussagenlogik. Eine davon soll höchstens einen Operator haben.
- In welcher Komplexitätsklasse ist das Erfüllbarkeitsproblem für 3-KNF? In welcher 2-KNF? Wie sieht es mit dem Allgemeingültigkeitsproblemen aus?
- Was ist der Shannon-Graph von \(1\)?
- Was ist der Shannon-Graph von \(0\)?
- Was ist der Shannon-Graph von \(a \lor b\)?
- Was ist der Shannon-Graph von \(a \land b\)?
Meine Fragen
- 02, Folie 19/29: Warum wird einmal \(\models\) und dann \(\models_\Sigma\) geschrieben?
- 07, Folie 19/51: Warum "fast alle" \(x \in Var\)? Was bedeutet das?
- Es dürfen nur endlich viele Variablen umbenannt bzw. durch einen Term ersetzt werden. Andernfalls werden die Beweise und Notationen hässlich. Abzählbar unendlich viele Variablen sind praktisch, wenn man sich die Existenz immer weiterer Variablen sichern will, die nicht in einer gegebenen Formel auftauchen. Natürlich ist jede Formel endlich, enthält also nur endlich viele Variablen.
- Folie 8/30: Wieso stimmt diese Umformung?
- Gebundene Variablen dürfen unabhängig von freien umbenannt werden. Die andere Umformung kann nachvollzogen werden, wenn die Implikation \(A \rightarrow B\) zu \(\neg A \vee B\) umgeformt wird. Man beachte folgende Umformungsregel: \(\neg \forall x F(x) \equiv \exists x \neg F(x)\).
- Folie 23/30: Was ist eine Grundinstanz? Wo ist der Unterschied zwischen "Grundinstanz" und "Instanz"? Was sind "Grundterme"?
- Grundterm: Ein Term, der keine Variablen enthält. Instanz: Für quantifizierte Variablen wurden Terme eingesetzt. Grundinstanz: Für alle Variablen wurden Grundterme eingesetzt. Damit enthalten Grundinstanzen überhaupt keine Variablen mehr.
- Folie 24/30: Was ist ein Beispiel für \(D = Term_\Sigma^0 \neq\) Menge der Grundterme? Wo gilt 2. nicht?
- Ich vermute mal, dass \(Term_\Sigma^0 := $ Menge der Grundterme. Bachte (sofern die Definition stimmt): $Term_\Sigma^0 \subseteq Term_\Sigma\), da es auch Terme gibt, die Variablen enthalten, falls welche in der Signatur vorhanden sind. Was ist die Bedeutung von Herbrand-Strukturen / dem Satz von Herbrand?
- Blatt 6, Lösung zu Aufgabe 4: Den Teil mit der Umwandlung einer Aussagenlogischen Formel verstehe ich nicht. Kann das jemand bitte für \(a \land \neg b \lor c \lor d\) erklären?
- Blatt 9, Lösung zu Aufgabe 1: Ist der Baum, also insbesondere die ersten 4 Knoten, richtig? Warum steht in Knoten 1 nicht \(1\forall x \forall y \forall z (r(x,y) \land r(y,z) \rightarrow r(x,z))\)? Wie funktioniert der 1. Schritt in Aufgabe 2?
- Haben reflexive Relationen irreduzible Elemente?
- Laut unserer Definition nicht. Aber du kannst jede n-stellige Relation mit dem Komplement der n-stelligen Gleichheits-Relation schneiden, dann erhältst du ihr irreflexives Gegenstück.
- Können reflexive Relationen noethersch sein?
- Nur, wenn sie leer sind. Ansonsten gibt es immer unendliche Ketten.
- Folie 27: Wie muss ich \(\square \diamond P\) lesen?
- Von jeder erreichbaren Welt aus gibt es eine erreichbare Welt, in der P gilt. Die Verbalisierung der Relation "erreichbar" klappt immer ;)
- Blatt 12, Aufgabe 1b: Was sagt \(\diamond\square P\) auf dem Graphen aus? Insbesondere: Warum ist \(w_5\) nicht in \(\diamond\square P\)? Was wäre \([[\square \diamond P]]\)?
- Blatt 12, Aufgabe 4: Das muss ich noch mal in Ruhe durchgehen.
- 21, Folie 8: Was ist \(Th(N)\) und was ist \(Cn(PA)\)?
- \(Th(N)\): Theoreme über N, also die Menge aller Formeln, für die die natürlichen Zahlen ein Modell sind. Cn(PA): Menge aller Formeln, die aus den Axiomen der Peano-Artihmetik gefolgert werden können. Da die Peano-Arithmetik korrekt ist, ist jede Formel aus Cn(PA) auch in Th(N).
- 50, Folie 16: Was bedeutet es, dass \(Th(N)\) nicht rekursiv ist?
- Rekursiv heißt entscheidbar. Da die Peano-Axiome durch die Peano-Artihmetik formalisiert werden können, gibt es eine Formel P(x), die genau dann wahr ist, wenn für x die Kodierung einer solchen Formel eingesetzt wird, die sich nicht aus den Peano-Axiomen herleiten lässt. Nach dem Gödelschen Unvollständigkeitssatz gibt es nun eine Formel P und x derart, dass x mit der Kodierung von P(x) übereinstimmt: Eine Formel also, die über sich selbst behauptet, sie sei nicht herleitbar. Da es nur ein Modell gibt, ist jede Formel entweder unerfüllbar oder allgemeingültig. Wenn \(Th(N)\) entscheidbar wäre und P(x) allgemeingültig, dann entsteht Widerspruch zur Wahl von P und x. Wenn P(x) unerfüllbar wäre, ist nach Wahl von P und x P(x) herleitbar, was wieder einen Widerspruch darstellt. Um den Widerspruch aufzulösen, darf "aus den PA-Axiomen herleitbar" nicht mit "im Modell der nat. Zahlen gültig" übersetzt werden.
- 23, Folie 5: Kann mir jemand ein konkretes Beispiel geben?
- 43, Folie 2: Was sind omega-Strutkuren und insbesondere was bedeutet \(2^P\)?
- Eine Omega Struktur Ordnet jedem Zeitpunkt, wenn die natürlichen Zahlen als Zeitstrahl aufgefasst werden, eine Menge von aussagenlogischen Variablen zu, die als "wahr" gelten sollen. \(2^P\) ist die Potenzmenge von P.
- Ist \(A\;\textbf{U}_W\;B\) äquivalent zu \(B\;\textbf{V}\;A\)?
- Blatt 14, 2a: Warum ist \(\diamond (p\;\textbf{U}\;q)\) äquivalent zu \(\diamond q\)? Ich dachte es wäre äquivalent zu \(p\;\textbf{U}\;q\)?
- Blatt 14, 3: Wie würde der Automat aussehen, wenn das \(X\) weggelassen würde?
- Blatt 14, 4: Das würde ich gerne gemeinsam durchgehen.
- 50, 13: Was sind die Ziele der Beweistheorie? Was ist die Grundidee des Hilbert-Kalküls?
- Ziele: Automatisches Beweisen ermöglichen und die Grenzen bestimmen. Grundidee des Hilbert-Kalküls: Aus Axiomen konstruktiv Formeln folgern. Im Gegensatz zu den praxis-orientierten Beweisverfahren kann der Hilbert-Kalkül leichter in theoretischen Beweisen verwendet werden. Der Gödelsche Unvollständigkeitssatz verwendet z.B. den Hilbert-Kalkül.
- 50, 13: "Aussagenlogische Tableauregeln aus Wahrheitstafeln konstruieren." - was ist damit gemeint?
- 50, 15: Was ist die Grundidee der Peano-Arithmetik?
- Liegt doch eigentlich auf der Hand: Zahlentheoretische Aussagen automatisch beweisen.
- 50, 33: Wie kann man sich in dem Beispiel den Unterschied zwischen Prädikaten und Funktionen erschließen?
- Funktionen sind immer in Prädikaten enthalten. Ein Prädikat darf kein weiteres Prädikat enthalten.
- Wie ist Erfüllbarkeit in der Prädikatenlogik definiert? Z.B. erscheint mir \(\exists x p(x)\) erfüllbar, wenn nichts weiter gegeben ist. Wenn man aber \(p(x)=False\) für alle \(x\) sagt, dann ist es unerfüllbar.
- F ist erfüllbar gdw. es ein Modell für F gibt, d.h. eine Interpretation I, sodass val_I(F) = W.
- Müssen die Kanten von Shannon-Graphen mit W und F oder mit 1 und 0 beschriftet werden? Praktisch alle Altklausuren verwenden 1 und 0, aber ich meine er hätte in der Vorlesung gesagt, dass wir W und F verwenden sollen.
- Ist die Menge der allgemeingültigen / erfüllbaren / unerfüllbaren Formeln der PL1 abzählbar? Jede Teilmenge aus \(\Sigma^*\) ist abzählbar für ein endliches Alphabet \(\Sigma\). Es gibt aber überabzählbar viele Teilmengen, deren Elemente zwar wieder abzählbar sind, aber sowohl die Teilmengen selbst als auch ihre Elemente nicht aufzählbar sind. Beachte: Aufzählbar \(\neq\) Abzählbar.
- Wie kann man \(U\) durch \(U_W\) darstellen?
Altklausuren
- WS2010/2011, 1. Zwischentest, A4: Ist der Markierungsalgorithmus für Hornformeln relevant?
- WS2010/2011, 2. Zwischentest, A1:
- Was ist eine kompakte Logik? (PL2 ist laut WS2008/2009, 2.Zwischentest 1b, nicht kompakt)
- Was bedeutet \(Cl_{\exists}(t_1 \doteq t_2)\)?
- WS2009/2010, A1c: Wieso gibt es für \(\exists p(x)\) kein Herbrandmodell?
- WS2009/2010, 1.Zwischentest
- A1a: Was ist ein "Vereinfachungsschritt" im Davis-Putnam-Verfahren? Was bedeutet es, wenn dort keine Klausel mehr zur Verfügung steht?
- A1a: "Wenn A und B erfüllbar sind, dann ist auch \(A \rightarrow B\) erfüllbar." - Was ist mit \(B = \neg A\)?
- WS 2009/2010, 2. Zwischentest (ist beim ersten):
- A1a: Warum ist \(\forall x \forall y (x \leftrightarrow y)\) keine Formel der PL1?
- A4: Will ich gerne durchsprechen
- WS 2008/2009:
- 1a: Warum ist \(\forall x (p(x) \rightarrow q(p(x)))\) keine Formel der PL1?
- 1a: Warum ist \(\exists x (p(x) \rightarrow p(f(x)))\) allgemeingültig?
- 1b: Was ist ein Beispiel für einen Büchi-Automaten, für den es keinen deterministischen Büchi-Automaten gibt?
- 1b: "Für jede geschlossene prädikatenlogische Formel G gilt: Es gibt ein Modell für G oder für das Negat von G oder für beide." - Gilt das nicht für alle prädikatenlogischen Formeln (egal ob geschlossen oder nicht)?
- WS 2008/2009, 1. Zwischentest:
- 1a: Wie lange dauert der kürzeste Resoultionsbeweis in Anzahl der Literale?
- 1b: Warum gibt es keine prädikatenlogische Interprätation, in der alle prädikatenlogischen Formeln wahr sind?
Material
StackExchange:
- What is the operator precedence for quantifiers?
- How do you bring quantors to the front of a formula?
- How to convert to conjunctive normal form?
Übungsbetrieb
- Wo sind die Übungsblätter: Link
- Abgabeform: Keine Abgabe
- Turnus: wöchentlich
- Lösungen: Die Lösungen von jeweils zwei Blättern werden dann in den 14-tägig stattfinden Übungen am Freitag besprochen.
- Übungsschein verpflichtend: Es gibt keinen Übungsschein.
- Bonus durch Übungsschein: Es gibt keinen Klausurbonus durch Übungsblätter.
- Anderer Klausurbonus: Man kann durch insgesammt 4 Zwischentests und 2 Praxisaufgaben für die wirkliche Klausur Punkte sammeln. Die Teilnahme an den Zwischentests und den Praxisaufgaben ist freiwillig. Die erzielten Übungspunkte werden im Verhältnis 1:10 als Bonuspunkte auf die bestandene Abschlussklausur angerechnet.
Termine und Klausurablauf
Siehe Klausurtermine-Seite für zukünftige Termine.
Datum: Freitag, den 6. März 2015 von 11:00 bis 12:00 Uhr (Quelle).
Ort: Gerthsen (30.21) und HSaF (50.35) - vgl. Anmeldeliste
Punkte: 60
Punkteverteilung: ? (Stand: 06.03.2015)
Bestehensgrenze: ? (Stand: 06.03.2015)
Übungsschein: Gibt es nicht.
Bonuspunkte: Bis zu 8. Die Punkte aus den 4 Zwischenprüfungen und 2 Praxisaufgaben werden addiert, dann durch 10 geteilt und schließlich kaufmännisch gerundet.
Ergebnisse: Klausur wurde noch nicht geschrieben
Einsicht: steht noch nicht fest (Stand: 06.03.2015)
Erlaubte Hilfsmittel: Keine.
Ergebnisse
Klausur wurde noch nicht geschrieben.