C2: Modellierung und Normalformen

• Heute wollen wir schauen was wann wie erfüllbar ist
• Die motivation dazu ist dieselbe wie das was wir schon bei aussagenlogik etc. gemacht haben
• das ist alles das gleiche, bis auf, dass das hier jetzt nen bissl komplizierter ist

Modellierung: Formeln erstellen und verstehen

• wir erinnern uns an das "tolle" schloss dreadsbury
• Da (und auch nur da) konnte man mit logischen formeln einen Mord aufklären
  • Das haben wir gemacht, indem wir die zwischenmenschlichen beziehungen mit prädikatenlogik formalisiert haben (was irgendwie nen sehr komisches verfahren ist)
  • Wir konnten mit so ausdrücken wie $\forall x\forall y(D(x)\to \neg K(y,x))$ definieren, dass niemand der im Schloss selber wohnt ermordet würde
• Diese formeln haben wir mithilfe von "aussagen" definiert die wir uns wie funktionen vorstellen können
  • dementsprechend gilt sowas wie $D(x)$ in unserem fall dafür, dass $x$ im Schloss wohnt
• So können wir auch komplexere sachverhalte "dynamisch" modellieren, indem wir aus diesen "simplen" Formeln komplexere zusammensetzen
• wir versuchen natürlich die sachen so zu modellieren, dass sie immernoch der "natürlichen sprache" ähneln, denn am besten modelliert man "nach der umgangssprache"
• Was dann noch für uns interessant ist, sind die "beschränkten quantoren"
• Diese sind in der mathematik sehr beliebt, da man mit diesen einfach einen Wertbereich einschränken kann
  • solche dinge sind bei uns aber leider nicht erlaubt
• Wir können aber statt sowas wie $\forall x(R(x)\to \psi )$ anstelle von $\forall x\in R:\psi$ schreiben
• Ebenso kann man $\exists x\in R:\psi$ durch $\exists x(R(x)\wedge \psi )$ ersetzen
• Damit simulieren wir eben diese "Beschränkten quantoren"

Äquivalenzen

• zuerst wollen wir uns aber dann mal anschauen wie wir bestimmen können, dass zwei aussagen äquivalent sind
• Denn beide sind Äquivalent, wenn es eine passende Interprätation $I$ gibt für die gilt, dass $I\models \phi \iff I\models \psi$
  • Das schreiben wir "einfacher" so: $\phi \equiv \psi$
• 
• 

Nachweise von Äquivalenzen

• Wir können äquivalenzen immer nachweisen indem wir
  • die Definition überprüfen
  • das ersetzungslemma
• Wasn das Ersetzungslemma?

• Sei ${\phi }_1$ eine prädikaten-logische Formel mit einer Teilformel ${\psi }_1$
• Sei ${\psi }_2$ eine weitere Formel mit ${\psi }_2\equiv ps{i}_1$
• Wenn ${\phi }_2$ aus ${\phi }_1$ entsteht, indem ein Vorkommen von ${\psi }_1$ durch ${\psi }_2$ ersetzt wird,
  dann gilt ${\phi }_2\equiv {\phi }_1$

• Hier gibts nen beispiel.

Nachweise von Nicht-Äquivalenz

• Wenn wir die Äquivalenz definieren können, müssen wir ja auch definieren können, dass man andere sachen nicht definieren kann
• Das machen wir (wie so oft) "einfach" mit nem gegenbeispiel
• 

Normalformen

• Was ist denn eine Normalform?
  • eine Prädikatenlogische Formel ist in reduzierter form wenn sie nur $\exists ,\vee ,\neg$ verwendet, aber bene nicht $\forall$ und $\wedge$
  • $\phi$ ist in Negationsnormalform (NNF), wenn Negationen in $\phi$ nur unmittelbar vor atomaren Formeln vorkommen
  • $\phi$ ist in prännexform wenn sie so aussieht: $Q_1{x}_1{Q}_2{x}_2...Q_k{x}_k{\phi }^{\prime }$
    • Dabei ist $Q_i$ entweder $\exists$ oder $\forall$
    • $x_i$ muss paarweise verschieden sein
    • ${\phi }^{\prime }$ quantorenfrei
  • Beispiel
• Umwandlung in Pränexform: ein Algorithmus
• Berechnung von einer Pränexform: Beispiel
• Berechnung von einer Pränexform: Beispiel 2

Erfüllbarkeitstest

• So wir wollen am ende ja auch testen, ob das was wir da gebastelt haben auch wirklich erfüllbar ist
• Erstmal wollen wir ein paar begriffe definieren:
  • Eine Interpretation $I$ von einem Modell $\phi$ heisst Modell von $\phi$, wenn $I\models \phi$ gilt.
  • Wenn $\phi$ ein Model hat, ist $\phi$ erfüllbar, sonst nicht
  • Wenn jede passende Interpretation von $\phi$ ein Modell von $\phi$ ist, ist $\phi$ allgemeingültig
    • Eine andere Bezeichnung für das ist die Tautologie
  • $I$ ist ein Nodell einer Menge prädikatenlogischer Formeln $\varphi$, falls $I\models \phi$ für alle $\phi \in \varphi$ gilt.
• Die Begriffe "erfüllbar" und "allgemeingültig" haben für Mengen von Formeln $\varphi$ die gleiche bedeutung
• Beispiele:
  • $\exists x\forall y(R(x)\vee \neg R(y))$ ist allgemeingültig
  • $\forall x\exists y(\neg R(x)\wedge R(y))$ ist unerfüllbar
• Anmerkungen:
  • Der Zusammenhang zwischen unerfüllbaren und allgemeingültigen Formeln ist genauso wie in der Aussagenlogik:
    $\phi$ unerfüllbar $\iff$ $\neg \phi$ allgemeingültig
  • Ist $\phi$ einge geschlossene Formel mit Modell $I=(\mathrm{A},\beta )$, so nennen wir auch $\mathrm{A}$ ein Modell von $\phi$ und schreiben $\mathrm{A}\models \phi$
• Fun-Fact: Der Unterschied zwischen $\phi$ und $\varphi$ ist, dass das erste als "die variable" Phi definiert wird und das andere dann als "das normale" Phi

Skolemform

• Wir wollen unsere bisherigen Formeln ein wenig vereinfachen, da diese ja teilweise schon sehr schnell sehr komplex werden können
  • Damit wollen wir dann die Erfüllbarkeit einfacher überprüfen können
  • Wir bemerken: Wenn wir die Erfüllbarkeit einer Formel $\phi$ testen wollen, können wir auch "einfach" eine "simplere" Formel $\psi$ aufstellen die sich was Erfüllbarkeit angeht gleich verhält, überprüfen
    • So können wir Quantoren "sparen"
  • Jetzt stellen wir uns aber die frage "Wann verhält sich denn eine Formel vor der Erfüllbarkeit gleich wie eine andere"?
    • Erstmal die komischen begriffe:
    • Wir nennen das Erfüllbarkeitsäquivalent
  • Zwei formeln sind Erfüllbarkeitsäquivalent, wenn:
    • $\phi$ und $\psi$ beide entweder erfüllbar oder beide nicht erfüllbar sind.
• Zurück zur Überschrift
• Eine prädikatenlogische Formel ist dann in Skolemform wenn sie
  • in Pränexform ist
  • im Quantoren-Präfix nur Allquantoren vorkommen
  • im Quantoren-Präfix keine Variable mehrfach vorkommt
• Allgemein gesagt sieht eine Formel in Skolemform also so aus: $\forall x_1...\forall x_n\psi$, wobei $\psi$ quantorenfreii ist
• Ein Beispiel
• Wenn wir die Skolemregel anwenden, können wir u.U. Existenzquantoren die "erfüllbarkeitsäquivalent" sind aus unserer Formel entfernen

Die Skolem-Regel

• Ist $\phi =\forall x_1\forall x_2...\forall x_k\exists y\psi$ und kommt das Funktionssymbol $f$ in $\psi$ nicht vor, so ist die Formel $\forall x_1\forall x_2...\forall x_k\psi [y/f(x_1,...,x_k)]$ erfüllbarkeitsäquivalent zu $\phi$
• Bemerkungen dazu:
  • $\psi$ darf weitere Quantoren enthalten
  • steht der $\exists$-Quantor am Anfang $(k=0)$, so wird $y$ durch eine Konstante ersetzt.
    • Wir erinnern uns: Konstanten sind eigentlich $0$-Stellige funktionen.
• ToDo: 26