Ist D eine Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$ und ist E eine Deduktion von $\psi$ mit Hypothesen aus $\Gamma$, so ergibt sich die folgende Deduktion von $\varphi\wedge\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\varphi\wedge\psi$ mit Hypothesen aus $\Gamma$, so ergeben sich die folgenden Deduktionen von $\varphi$ bzw. von $\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\psi$ mit Hypothesen aus $\Gamma\cup\{\varphi\}$, so ergibt sich die folgende Deduktion von $\varphi\rightarrow\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$ und ist E eine Deduktion von $\varphi\rightarrow\psi$ mit Hypothesen aus $\Gamma$, so ergibt sich die folgende Deduktion von $\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\varphi\vee\psi$ mit Hypothesen aus $\Gamma$, ist E eine Deduktion von $\sigma$ mit Hypothesen aus $\Gamma\cup\{\varphi\}$und ist F eine Deduktion von $\sigma$ mit Hypothesen aus $\Gamma\cup\{\psi\}$, so ergibt sich die folgende Deduktion von $\sigma$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\bot$ mit Hypothesen aus $\Gamma\cup\{\varphi\}$, so ergibt sich die folgende Deduktion von $\lnot\varphi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\lnot\varphi$ mit Hypothesen aus $\Gamma$ und ist E eine Deduktion von $\varphi$ mit Hypothesen aus $\gamma$, so ergibt sich die folgende Deduktion von $\bot$ mit Hypothesen aus $\Gamma$:
ausführlich: Ist D eine Deduktion von $\bot$ mit Hypothesen aus $\Gamma$, so ergibt sich die folgende Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$:
\begin{flashcard}[ Natürliches Schließen ]{ reductio ad absurdum }
Ist D eine Deduktion von $\bot$ mit Hypothesen aus $\Gamma\cup\{\lnot\varphi\}$, so ergibt sich die folgende Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$:
Für eine Formelmenge $\Gamma$ und eine Formel $\varphi$ schreiben wir $\Gamma\Vdash\varphi$ wenn es eine Deduktion gibt mit Hypothesen aus $\Gamma$ und Konklusion $\varphi$. Wir sagen "$\varphi$ ist eine syntaktische Folgerung von $\Gamma$".
Eine Formel $\varphi$ ist ein Theorem, wenn $\varnothing\Vdash\varphi$ gilt.
$\Gamma\Vdash\varphi$ sagt (zunächst) nichts über den Inhalt der Formeln in $\Gamma\cup\{\varphi\}$ aus, sondern nur über die Tatsache, dass $\varphi$ mithilfe des natürlichen Schließens aus den Formeln aus $\Gamma$ hergeleitet werden kann.
Ebenso sagt "$\varphi$ ist Theorem" nur, dass $\varphi$ abgeleitet werden kann, über "Wahrheit" sagt dieser Begriff (zunächst) nichts aus.
$A\subseteq\mathbb{R}$ ist ,,Menge der Menschen, die Aussage für wahr halten''
\end{flashcard}
\begin{flashcard}[ Semantik ]{ Heyting-Algebra }
$H_R$= Menge der offenen Teilmengen von $\mathbb{R}$
Erinnerung: $A\subseteq\mathbb{R}$ offen, wenn $\forall a\in A\exists\epsilon >0:(a-\epsilon,a+\epsilon)\subseteq A$, d.h. wenn $A$ abzählbare Vereinigung von offenen Intervallen $(x,y)$ ist.
\end{flashcard}
\begin{flashcard}[ Semantik ]{ offen vs. nicht offene Teilmengen }
$(W,\leq)$ partiell geordnete Menge, $M\subseteq W$ und $a\in W$
a ist kleinste obere Schranke/Supremum von $M$, wenn $a$ obere Schranke von $M$ ist und wenn $a\leq b$ für alle oberen Schranken $b$ von $M$ gilt. Wir schreiben in diesem Fall $a=sup\ M$.
z.B. $(W,\leq)$ mit $W=R$ und $\leq$ übliche Ordnung auf R
\begin{itemize*}
\item dann gelten sup[0, 1] = sup(0, 1) = 1.
\item$sup\ W$ existiert nicht (W keine obere Schranke)
Sei $(W,\leq)$ partiell geordnete Menge, $M\subseteq W$ und $a\in W$.
a ist untere Schranke von $M$, wenn $a\leq m$ für alle $m\in M$ gilt.
\end{flashcard}
\begin{flashcard}[ Wahrheitswertebereiche ]{ größte untere Schranke }
Sei $(W,\leq)$ partiell geordnete Menge, $M\subseteq W$ und $a\in W$.
a ist größte untere Schranke oder Infimum von $M$, wenn a untere Schranke von $M$ ist und wenn $b\leq a$ für alle unteren Schranken $b$ von $M$ gilt. Wir schreiben in diesem Fall $a=inf\ M$.
Ein (vollständiger) Verband ist eine partiell geordnete Menge $(W,\leq)$, in der jede Menge $M\subseteq W$ ein Supremum $sup\ M$ und ein Infimum $inf\ M$ hat. In einem Verband $(W,\leq)$ definieren wir:
\begin{itemize*}
\item$0_W = inf\ W$ und $1_W= sup\ W$
\item$a\wedge_W b= inf\{a,b\}$ und $a\vee_W b= sup\{a,b\}$ für $a,b\in W$
\end{itemize*}
In jedem Verband $(W,\leq)$ gelten $0_W= sup\ \varnothing$ und $1_W= inf\ \varnothing$ (denn jedes Element von $W$ ist obere und untere Schranke von $\varnothing$).
Ein Wahrheitswertebereich ist ein Tupel $(W,\leq,\rightarrow W,\lnot W)$, wobei $(W,\leq)$ ein Verband und $\rightarrow W:W^2\rightarrow W$ und $\lnot W:W\rightarrow W$ Funktionen sind.
Der Boolesche Wahrheitswertebereich B ist definiert durch die Grundmenge $B=\{0,1\}$, die natürliche Ordnung $\leq$ und die Funktionen $\lnot_B (a)=1-a$, $\rightarrow_B(a,b)= max(b, 1-a)$. Hier gelten:
Der Kleenesche Wahrheitswertebereich $K_3$ ist definiert durch die Grundmenge $K_3=\{0,\frac{1}{2},1\}$ mit der natürlichen Ordnung $\leq$ und durch die Funktionen $\lnot_{K_3}(a)=1-a $, $\rightarrow_{K_3}(a,b)= max(b, 1-a)$. Hier gelten:
Der Wahrheitswertebereich F der Fuzzy-Logik ist definiert durch die Grundmenge $F=[0,1]\subseteq\mathbb{R}$ mit der natürlichen Ordnung $\leq$ und durch die Funktionen $\lnot_F (a)=1-a$, $\rightarrow_F (a,b)= max(b, 1-a)$. Hier gelten:
Der Boolesche Wahrheitswertebereich $B_R$ ist definiert durch die Grundmenge $B_R=\{A|A\subseteq\mathbb{R}\}$ mit der Ordnung $\subseteq$ und durch die Funktionen $\lnot_{B_R}(A)=\mathbb{R}\backslash A$, $\rightarrow_{B_R}(A,B)= B\cup\mathbb{R}\backslash A$. Hier gelten:
Der Heytingsche Wahrheitswertebereich $H_R$ ist definiert durch die Grundmenge $H_{\mathbb{R}}=\{A\subseteq\mathbb{R} | \text{A ist offen}\}$, die Ordnung $\subseteq$ und durch die Funktionen $\lnot_{H_R}(A)= Inneres(\mathbb{R}\backslash A)$, $\rightarrow_{H_R}(A,B)=Inneres(B\cup\mathbb{R}\backslash A)$. Hier gelten:
Eine Formel $\phi$ heißt eine W-Folgerung der Formelmenge $\Gamma$, falls für jede W-Belegung B, die zu allen Formeln aus $\Gamma\cup\{\phi\}$ paßt, gilt:
$inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\phi)$
Wir schreiben $\Gamma\Vdash W\phi$, falls $\phi$ eine W-Folgerung von $\Gamma$ ist.
Bemerkung: Im Gegensatz zur Beziehung $\Gamma\vdash\phi$, d.h. zur syntaktischen Folgerung, ist $\Gamma\Vdash W \phi$ eine semantische Beziehung.
Eine W-Tautologie ist eine Formel $\phi$ mit $\varnothing\Vdash W\phi$, d.h. $B(\phi)=1_W$ für alle passenden W-Belegungen B (denn $inf\{\hat{B}(\gamma)|\gamma\in\varnothing\}= inf \varnothing=1_W)$.
\end{flashcard}
\begin{flashcard}[ Wahrheitswertebereiche ]{$\varnothing\Vdash_W\lnot\lnot\phi\rightarrow\phi$ gilt für Wahrheitsbereiche... }
\begin{flashcard}[ Korrekheit ]{ Frage der Korrektheit }
Können wir durch mathematische Beweise zu falschen Aussagenkommen?
Können wir durch das natürliche Schließen zu falschen Aussagen kommen?
Existiert eine Menge $\Gamma$ von Formeln und eine Formel $\varphi$ mit $\Gamma\vdash\varphi$ und $\Gamma\not\Vdash_W \varphi$? Für welche Wahrheitswertebereiche W?
Für welche Wahrheitswertebereiche W gilt $$\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_W \varphi$$ bzw. $\varphi$ ist Theorem $\Rightarrow\varphi$ ist W-Tautologie?
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Korrektheitslemma für nat. Schließen \& Wahrheitswertebereich B }
Sei $D$ eine Deduktion mit Hypothesen in der Menge $\Gamma$ und Konklusion $\varphi$. Dann gilt $\Gamma\vdash_B \varphi$, d.h. $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\varphi)$ für alle passenden B-Belegungen $B$.
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Korrektheitssatz für natürliches Schließen \& Wahrheitswertebereich $B$}
Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_B\varphi$.
Beweis: Wegen $\Gamma\vdash\varphi$ existiert eine Deduktion $D$ mit Hypothesen in $\Gamma$ und Konklusion $\varphi$. Nach dem Korrektheitslemma folgt $\Gamma\vdash_B \varphi$.
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Jedes Theorem ist eine B-Tautologie? }
wahr
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Korrektheitssatz für natürliches Schließen \& Wahrheitswertebereich $B_\mathbb{R}$}
Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_{B_\mathbb{R}}\varphi$.
Definition
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Jedes Theorem ist eine $B_\mathbb{R}$-Tautologie? }
wahr
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Korrektheitslemma für nat. Schließen \& Wahrheitswertebereich $H_{\mathbb{R}}$}
Sei $D$ eine Deduktion mit Hypothesen in der Menge $\Gamma$ und Konklusion $\varphi$, die die Regel $(raa)$ nicht verwendet. Dann gilt $\Gamma\vdash_{H_\mathbb{R}}\varphi$.
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Korrektheitssatz für nat. Schließen \& Wahrheitswertebereich $H_{\mathbb{R}}$}
Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt $\Gamma\vdash\varphi$ ohne $(raa)$$\Rightarrow\Gamma\vdash_{H_{\mathbb{R}}}\varphi$
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Jedes $(raa)$-frei herleitbare Theorem ist eine $H_{\mathbb{R}}$-Tautologie? }
wahr
\end{flashcard}
\begin{flashcard}[ Korrekheit ]{ Deduktion von Thermen ohne Hypothesen mit (raa) }
Jede Deduktion der Theoreme $\lnot\lnot\varphi\rightarrow\varphi$ und $\varphi\vee\lnot\varphi$ ohne Hypothesen verwendet $(raa)$.
\end{flashcard}
\begin{flashcard}[ Vollständigkeit ]{ Frage der Vollständigkeit }
Können wir durch mathematische Beweise zu allen korrekten Aussagen kommen?
Können wir durch das natürliche Schließen zu allen korrekten Aussagen kommen?
Existiert eine Menge $\Gamma$ von Formeln und eine Formel $\varphi$ mit $\Gamma\vdash_W\varphi$ und $\Gamma\not\vdash\varphi$? Für welche Wahrheitswertebereiche $W$?
Für welche Wahrheitswertebereiche $W$ gilt $\Gamma\vdash_W \varphi\Rightarrow\Gamma\vdash\varphi$ bzw. $\varphi$ ist $W$-Tautologie $\Rightarrow\varphi$ ist Theorem?
Sei $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\not\vdash\varphi\Leftrightarrow\Gamma\cup\{\lnot\varphi\}$ konsistent.
Jede konsistente Formelmenge $\Gamma$ ist in einer maximal konsistenten Formelmenge $\Delta$ enthalten.
\end{flashcard}
\begin{flashcard}[ Vollständigkeit ]{ Sei $\Delta$ maximal konsistent und gelte $\Delta\vdash\varphi$}
Sei $\Delta$ maximal konsistent und gelte $\Delta\vdash\varphi$. Dann gilt $\varphi\in\Delta$.
\end{flashcard}
\begin{flashcard}[ Vollständigkeit ]{ Sei $\Delta$ maximal konsistent und $\varphi$ Formel }
Sei $\Delta$ maximal konsistent und $\varphi$ Formel. Dann gilt $\varphi\not\in\Delta\Leftrightarrow\lnot\varphi\in\Delta$.
\end{flashcard}
\begin{flashcard}[ Erfüllbare Mengen ]{$\Gamma$ heißt erfüllbar, wenn }
Sei $\Gamma$ eine Menge von Formeln. $\Gamma$ heißt erfüllbar, wenn es eine passende B-Belegung $B$ gibt mit $B(\gamma)=1_B$ für alle $\gamma\in\Gamma$.
Die Erfüllbarkeit einer endlichen Menge $\Gamma$ ist entscheidbar (NP-vollständig)
Sei $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\not\Vdash_B\varphi\Leftrightarrow\Gamma\cup\{\lnot\varphi\}$ erfüllbar.
Sei $W$ einer der Wahrheitswertebereiche $B, K_3, F, H_R$ und $B_R,\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\Vdash W\varphi\Rightarrow\Gamma\Vdash B\varphi$.
Sei $\Gamma$ eine Menge von Formeln, $\varphi$ eine Formel und $W$ einer der Wahrheitswertebereiche $B,K_3 , F, B_R$ und $H_R$. Dann gilt $\Gamma\Vdash_W\varphi\Rightarrow\Gamma\vdash\varphi$.
Insbesondere ist jede W-Tautologie ein Theorem.
\end{flashcard}
\begin{flashcard}[ Vollständigkeit und Korrektheit ]{ Satz $\Gamma\vdash\varphi\Leftrightarrow\Gamma\Vdash_B \varphi$}
Seien $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $$\Gamma\vdash\varphi\Leftrightarrow\Gamma\Vdash_B \varphi$$
Insbesondere ist eine Formel genau dann eine B-Tautologie, wenn sie ein Theorem ist.
\begin{itemize*}
\item gilt für jede ,,Boolesche Algebra'', z.B. $B_R$
\item$\Gamma\vdash\varphi$ ohne ($raa$) $\Leftrightarrow\Gamma\Vdash_{H_R}\varphi$ (Tarksi 1938)
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Entscheidbarkeit ]{ Satz Menge der Theoreme }
Satz: die Menge der Theoreme ist entscheidbar.
\end{flashcard}
\begin{flashcard}[ Vollständigkeit und Korrektheit ]{ Äquivalenzen und Theoreme }
Zwei Formeln $\alpha$ und $\beta$ heißen äquivalent $(\alpha\equiv\beta)$, wenn für alle passenden B-Belegungen $B$ gilt: $B(\alpha)=B(\beta)$.
\end{flashcard}
\begin{flashcard}[ Vollständigkeit und Korrektheit ]{ Liste der Äquivalenzen 1/2 }
Sei $\Gamma$ eine u.U. unendliche Menge von Formeln und $\varphi$ eine Formel mit $\Gamma\Vdash_B\varphi$. Dann existiert $\Gamma'\subseteq\Gamma$ endlich mit $\Gamma'\Vdash_B \varphi$.
\end{flashcard}
\begin{flashcard}[ Kompaktheitsatzes ]{ Kompaktheits- oder Endlichkeitssatz }
Sei $\Gamma$ eine u.U. unendliche Menge von Formeln. Dann gilt $\Gamma$ unerfüllbar $\Leftrightarrow\exists\Gamma'\subseteq\Gamma$ endlich: $\Gamma'$ unerfüllbar
Ein Graph ist ein Paar $G=(V,E)$ mit einer Menge $V$
und $E\subseteq\binom{V}{2}=\{X\subseteq V:|V\Vdash2\}$.
Für $W\subseteq V$ sei $G\upharpoonright_W=(W,E\cap\binom{W}{2})$ der von $W$ induzierte Teilgraph.
Der Graph G ist 3-färbbar, wenn es eine Abbildung $f:V\rightarrow\{1,2,3\}$ mit $f(v)\not=f(w)$ für alle $\{v,w\}\in E$.
Bemerkung: Die 3-Färbbarkeit eines endlichen Graphen ist NP-vollständig
\end{flashcard}
\begin{flashcard}[ Kompaktheitsatzes ]{ Sei $G=(N,E)$ ein Graph }
Sei $G=(N,E)$ ein Graph. Dann sind äquivalent
\begin{enumerate*}
\item$G$ ist 3-färbbar.
\item Für jede endliche Menge $W\subseteq N$ ist $G\upharpoonright_W$ 3-färbbar.
\end{enumerate*}
\end{flashcard}
\begin{flashcard}[ Kompaktheitsatzes ]{ Parkettierungen Idee }
Gegeben ist eine Menge von quadratischen Kacheln mit gefärbten Kanten. Ist es möglich, mit diesen Kacheln die gesamte Ebene zu füllen, so dass aneinanderstoßende Kanten gleichfarbig sind?
Sei $K$ ein Kachelsystem. Es existiert genau dann eine Kachelung von $Z\times Z$, wenn für jedes $n\in N$ eine Kachelung von $\{(i,j) :|i|,|j| \leq n\}$ existiert.
Frage: existiert eine B-Belegung $B$ mit $B(\Gamma)=1_B$.
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ Hornklausel }
Eine Hornklausel hat die Form $(\lnot\bot\wedge p_1\wedge p_2\wedge ... \wedge p_n)\rightarrow q$ für $n\geq0$, atomare Formeln $p_1 ,p_2 ,... ,p_n$ und $q$ atomare Formel oder $q=\bot$. In der Literatur auch:
\begin{itemize*}
\item$\{\lnot p_1,\lnot p_2 ,... ,\lnot p_n,q\}$ für $\{p_1 ,... ,p_n\}\rightarrow q$ mit $q$ atomare Formel
\item$\{\lnot p_1,\lnot p_2 ,... ,\lnot p_n\}$ für $\{p_1 ,... ,p_n\}\rightarrow\bot$
\item$\Box$ für $\varnothing\rightarrow\bot$, die ,,leere Hornklausel''
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ Hornformel }
Eine Hornformel ist eine Konjunktion von Hornklauseln.
Eingabe: eine endliche Menge $\Gamma$ von Hornklauseln.
\begin{enumerate*}
\item\textbf{while} es gibt in $\Gamma$ eine Hornklausel $M\rightarrow q$, so daß alle $p\in M$ markiert sind und $q$ unmarkierte atomare Formel ist $\Rightarrow$\textbf{do} markiere $q$ (in allen Hornklauseln in $\Gamma$)
\item\textbf{if}$\Gamma$ enthält eine Hornklausel der Form $M\rightarrow\bot$, in der alle $p\in M$ markiert sind
\textbf{then} return ,,unerfüllbar''
\textbf{else} return ,,erfüllbar''
\end{enumerate*}
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ Terminierung endlicher Menge von Hornklauseln }
Sei $\Gamma$ endliche Menge von Hornklauseln. Dann terminiert der Markierungsalgorithmus mit dem korrekten Ergebnis.
Sei $\Gamma$ eine Menge von Hornklauseln. Eine SLD-Resolution aus $\Gamma$ ist eine Folge $(M_0\rightarrow\bot,M_1\rightarrow\bot,... ,M_m\rightarrow\bot)$ von Hornklauseln mit
\begin{itemize*}
\item$(M_0\rightarrow\bot)\in\Gamma$
\item für alle $0\leq n<m$ existiert $(N\rightarrow q)\in\Gamma$ mit $q\in M_n$ und $M_{n+1}= M_n\backslash\{q\}\cup N$
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ SLD-Resolution Beispiel \newline$\Gamma=\{\{BH\}\rightarrow AK,\{AK,BH\}\rightarrow\bot,\{RL,AK\}\rightarrow BH,\varnothing\rightarrow RL,\varnothing\rightarrow AK\}$}
\begin{flashcard}[ Erfüllbarkeit ]{ Lemma A: $\Gamma$ nicht erfüllbar }
Sei $\Gamma$ eine (u.U. unendliche) Menge von Hornklauseln und $(M_0\rightarrow\bot, M_1\rightarrow\bot,... , M_m\rightarrow\bot)$ eine SLD-Resolution aus $\Gamma$ mit $M_m=\varnothing$. Dann ist $\Gamma$ nicht erfüllbar.
Sei $\Gamma$ eine (u.U. unendliche) unerfüllbare Menge von Hornklauseln. Dann existiert eine SLD-Resolution $(M_0\rightarrow\bot,...,M_m\rightarrow\bot)$ aus $\Gamma$ mit $M_m=\varnothing$.
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ Satz Äquivalenz bei Hornklauseln }
Sei $\Gamma$ eine (u.U. unendliche) Menge von Hornklauseln. Dann sind äquivalent:
\begin{enumerate*}
\item$\Gamma$ ist nicht erfüllbar.
\item Es gibt eine SLD-Resolution $(M_0\rightarrow\bot,M_1\rightarrow\bot,... ,M_m\rightarrow\bot)$ aus $\Gamma$ mit $M_m=\varnothing$.
\end{enumerate*}
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ SLD-Resolution mit Breitensuche }
\begin{itemize*}
\item findet SLD-Resolution mit $M_m=\varnothing$ (falls sie existiert), da Baum endlich verzweigend ist (d.h. die Niveaus sind endlich)
\item hoher Platzbedarf, da ganze Niveaus abgespeichert werden müssen (in einem Binärbaum der Tiefe $n$ kann es Niveaus der Größe $2^n$ geben)
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Erfüllbarkeit ]{ SLD-Resolution mit Tiefensuche }
\begin{itemize*}
\item geringerer Platzbedarf (in einem Binärbaum der Tiefe $n$ hat jeder Ast die Länge $\leq n$)
\item findet existierende SLD-Resolution mit $M_m=\varnothing$ nicht immer
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{ aussagenlogische Formel daß der Graph eine Kante enthält }
Die aussagenlogische Formel $\bigvee_{1\leq i,j\leq9}\varphi_{i,j}$ sagt aus, daß der Graph eine Kante enthält.
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{ aussagenlogische Formel daß jeder Knoten einen Nachbarn hat }
Die aussagenlogische Formel $\bigwedge_{1\leq i\leq9}\bigvee_{1\leq j\leq9}\varphi_{i,j}$ sagt aus, daß jeder Knoten einen Nachbarn hat
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{ aussagenlogische Formel daß der Graph ein Dreieck enthält }
Die aussagenlogische Formel $\bigvee_{1\leq i,j,k\leq9\ verschieden}\varphi_{i,j}\wedge\varphi_{j,k}\wedge\varphi_{k,i}$ sagt aus, daß der Graph ein Dreieck enthält.
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{ Kodierung in einer ,,Struktur'' aus }
Eine Signatur ist ein Tripel $\sum=(\Omega, Rel,ar)$, wobei $\Omega$ und $Rel$ disjunkte Mengen von Funktions- und Relationsnamen sind und $ar:\Omega\cup Rel\rightarrow\mathbb{N}$ eine Abbildung ist.
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{ Menge der Variablen }
Die Menge der Variablen ist $Var=\{x_0,x_1 ,...\}$.
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{ Menge der $\sum$-Terme }
Sei $\sum$ eine Signatur. Die Menge $T_{\sum}$ der $\sum$-Terme ist induktiv definiert:
\begin{enumerate*}
\item Jede Variable ist ein Term, d.h. $Var\subseteq T_{\sum}$
\item ist $f\in\Omega$ mit $ar(f)=k$ und sind $t_1,...,t_k\in T_{\sum}$, so gilt $f(t_1,...,t_k)\in T_{\sum}$
\item Nichts ist $\sum$-Term, was sich nicht mittels der obigen Regeln erzeugen läßt.
Sei $\sum$ eine Signatur. Eine $\sum$-Struktur ist ein Tupel $A=(U_A,(f^A)_{f\in\Omega},(R^A)_{R\in Rel})$, wobei
\begin{itemize*}
\item$U_A$ eine nichtleere Menge, das Universum,
\item$R^A\supseteq U_A^{ar(R)}$ eine Relation der Stelligkeit $ar(R)$ für $R\in Rel$ und
\item$f^A:U_A^{ar(f)}\rightarrow U_A$ eine Funktion der Stelligkeit $ar(f)$ für $f\in\Omega$ ist.
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{$\sum$-Struktur mit $U_A^0=\{()\}$}
Bemerkung: $U_A^0=\{()\}$.
\begin{itemize*}
\item Also ist $a^A:U_A^0\rightarrow U_A$ für $a\in\Omega$ mit $ar(a)=0$ vollständig gegeben durch $a^A(())\in U_A$. Wir behandeln 0-stellige Funktionen daher als Konstanten.
\item Weiterhin gilt $R^A=\varnothing$ oder $R^A=\{()\}$ für $R\in Rel$ mit $ar(R)=0$.
\end{itemize*}
\end{flashcard}
\begin{flashcard}[ Prädikatenlogik ]{$A$ ist Modell von $\varphi$}
Sei $\sum$ eine Signatur, $\varphi$ eine $\sum$-Formel, $\Delta$ eine Menge von $\sum$-Formeln und $A$ eine $\sum$-Struktur.
\begin{itemize*}
\item$A\Vdash\varphi$ ($A$ ist Modell von $\varphi$) falls $A\Vdash_p\varphi$ für alle Variableninterpretationen $\rho$ gilt.
\item$A\Vdash\Delta$ falls $A\Vdash\Psi$ für alle $\Psi\in\Delta$.
