diff --git a/info4/kapitel-0/Logik.ipynb b/info4/kapitel-0/Logik.ipynb
index 86f827479cbc3f82966c90ba05523626714438b6..705e863e85f503f6e31fe71d3f07e50c44bd22c7 100644
--- a/info4/kapitel-0/Logik.ipynb
+++ b/info4/kapitel-0/Logik.ipynb
@@ -15,8 +15,13 @@
"Hier definieren wir einige Grundlagen und Notationen die im Skript verwendet werden.\n",
"Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.\n",
"\n",
- "Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [Gitlab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich.\n",
- "\n",
+ "Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [Gitlab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich.\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"## Was ist ein Notebook?\n",
"\n",
"* Dokument mit Text und ausführbaren Code-Abschnitten\n",
@@ -28,8 +33,13 @@
" * Speicherbar als Datei\n",
" * Code kann später neu ausgeführt werden\n",
" * Weitergabe an andere Nutzer möglich\n",
- "* Implementierungen: Mathematica, Maple, Jupyter, u. a.\n",
- "\n",
+ "* Implementierungen: Mathematica, Maple, Jupyter, u. a."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"## Jupyter Notebook\n",
"\n",
"* Browserbasierte Notebook-Oberfläche\n",
@@ -42,7 +52,13 @@
" * Ein sprachspezifischer **Kernel** stellt die Sprache dem Frontend zur Verfügung\n",
"* Schnittstellen zwischen Frontend und Kernel sind sprachneutral\n",
" * Kernel können in (fast) jeder Sprache implementiert werden, kein Python-Code nötig\n",
- " \n",
+ " "
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"## [ProB](https://www3.hhu.de/stups/prob) Kernel\n",
"\n",
"\n",
@@ -133,7 +149,7 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 30,
"metadata": {},
"outputs": [
{
@@ -145,7 +161,7 @@
"TRUE"
]
},
- "execution_count": 1,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -156,7 +172,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
@@ -168,7 +184,7 @@
"TRUE"
]
},
- "execution_count": 2,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
@@ -179,7 +195,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
@@ -191,7 +207,7 @@
"FALSE"
]
},
- "execution_count": 3,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
@@ -214,7 +230,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -226,7 +242,7 @@
"TRUE"
]
},
- "execution_count": 5,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -251,7 +267,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -263,7 +279,7 @@
"TRUE"
]
},
- "execution_count": 8,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -274,7 +290,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 35,
"metadata": {},
"outputs": [
{
@@ -286,7 +302,7 @@
"FALSE"
]
},
- "execution_count": 5,
+ "execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
@@ -304,7 +320,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
@@ -316,7 +332,7 @@
"TRUE"
]
},
- "execution_count": 12,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
@@ -327,7 +343,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 37,
"metadata": {},
"outputs": [
{
@@ -339,7 +355,7 @@
"TRUE"
]
},
- "execution_count": 6,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
@@ -357,7 +373,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 38,
"metadata": {},
"outputs": [
{
@@ -369,7 +385,7 @@
"TRUE"
]
},
- "execution_count": 18,
+ "execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@@ -380,7 +396,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
@@ -392,7 +408,7 @@
"TRUE"
]
},
- "execution_count": 17,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@@ -403,7 +419,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 40,
"metadata": {},
"outputs": [
{
@@ -415,7 +431,7 @@
"FALSE"
]
},
- "execution_count": 7,
+ "execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@@ -433,7 +449,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 41,
"metadata": {},
"outputs": [
{
@@ -445,7 +461,7 @@
"TRUE"
]
},
- "execution_count": 20,
+ "execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
@@ -456,7 +472,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 42,
"metadata": {},
"outputs": [
{
@@ -468,7 +484,7 @@
"TRUE"
]
},
- "execution_count": 21,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -479,7 +495,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 43,
"metadata": {},
"outputs": [
{
@@ -491,7 +507,7 @@
"FALSE"
]
},
- "execution_count": 26,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -515,7 +531,7 @@
},
{
"cell_type": "code",
- "execution_count": 58,
+ "execution_count": 44,
"metadata": {},
"outputs": [
{
@@ -524,7 +540,7 @@
"Preference changed: OPTIMIZE_AST = FALSE\n"
]
},
- "execution_count": 58,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -535,7 +551,7 @@
},
{
"cell_type": "code",
- "execution_count": 60,
+ "execution_count": 45,
"metadata": {},
"outputs": [
{
@@ -757,7 +773,7 @@
"<Dot visualization: formula_tree [(2>3 => 4>1) <=> not(5<1)]>"
]
},
- "execution_count": 60,
+ "execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
@@ -779,6 +795,15 @@
"Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \\vee (\\neg p \\wedge q)$?\n",
"\n",
"\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "## Interpretationen\n",
"Man braucht erst die Wahrheitswerte für die atomaren Aussagen $p$ und $q$.\n",
"Diese Information nennt man eine <b>Interpretation</b> für die Formel.\n",
"Die Formel oben hat 4 Interpretationen, da $p$ und $q$ jeweils wahr oder falsch sein können.\n",
@@ -795,7 +820,15 @@
"* Schritt 3: $FALSE \\wedge FALSE = FALSE$: $(TRUE \\vee FALSE)$\n",
"* Schritt 3: $TRUE \\vee FALSE = TRUE$: $TRUE$\n",
"\n",
- "Unter der Interpretation $i$ ist die Formel $(p \\vee (\\neg p \\wedge q)$ wahr.\n",
+ "Unter der Interpretation $i$ ist die Formel $(p \\vee (\\neg p \\wedge q)$ wahr."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Modelle\n",
+ "\n",
"Man nennt so eine Interpretation ein <b>Modell</b> für die Formel.\n",
"\n",
"* eine Interpretation $i$ so dass $i(\\phi)={\\color{olive} TRUE}$ ist ein <b>Modell</b> für $\\phi$\n",
@@ -809,8 +842,13 @@
"Die Formel ist also keine Tautologie, aber erfüllbar.\n",
"\n",
"Die Formel $p \\vee \\neg p$ ist eine Tautologie: alle Interpretation machen die Formel wahr.\n",
- "$p \\wedge \\neg p$ hingegen ist ein Widerspruch und hat kein Modell.\n",
- "\n",
+ "$p \\wedge \\neg p$ hingegen ist ein Widerspruch und hat kein Modell."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"# Äquivalenz von Formeln\n",
"\n",
@@ -822,7 +860,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 47,
"metadata": {},
"outputs": [
{
@@ -843,7 +881,7 @@
"TRUE\tTRUE\tTRUE\tTRUE\n"
]
},
- "execution_count": 37,
+ "execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
@@ -864,8 +902,13 @@
"Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man ```p=TRUE``` schreiben und anstatt $p \\vee q$ muss man ```p=TRUE ∨ q=TRUE``` schreiben. Mit ```bool(P)``` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um.\n",
"\n",
"$\\equiv$ ist eine Relation zwischen logischen Formeln.\n",
- "$\\equiv$ ist transitiv und kommutativ.\n",
- "\n",
+ "$\\equiv$ ist transitiv und kommutativ."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"# Wichtige Äquivalenzen\n",
"Für alle Formeln $\\phi, \\psi$ der Aussagenlogik gilt:\n",
"* $\\phi \\wedge \\psi \\equiv \\psi \\wedge \\phi$ (Kommutativität)\n",
@@ -885,32 +928,9 @@
},
{
"cell_type": "code",
- "execution_count": 71,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|p|q|ODER|NODER|NUND|np|nq|\n",
- "|---|---|---|---|---|---|---|\n",
- "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
- ],
- "text/plain": [
- "p\tq\tODER\tNODER\tNUND\tnp\tnq\n",
- "FALSE\tFALSE\tFALSE\tTRUE\tTRUE\tTRUE\tTRUE\n",
- "FALSE\tTRUE\tTRUE\tFALSE\tFALSE\tTRUE\tFALSE\n",
- "TRUE\tFALSE\tTRUE\tFALSE\tFALSE\tFALSE\tTRUE\n",
- "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\tFALSE\tFALSE\n"
- ]
- },
- "execution_count": 71,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {p,q,ODER,NODER,NUND,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &\n",
" ODER=bool(p=TRUE ∨ q=TRUE) &\n",
@@ -932,32 +952,9 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|p|q|IMPL|KONT|np|nq|\n",
- "|---|---|---|---|---|---|\n",
- "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
- ],
- "text/plain": [
- "p\tq\tIMPL\tKONT\tnp\tnq\n",
- "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\tTRUE\n",
- "FALSE\tTRUE\tTRUE\tTRUE\tTRUE\tFALSE\n",
- "TRUE\tFALSE\tFALSE\tFALSE\tFALSE\tTRUE\n",
- "TRUE\tTRUE\tTRUE\tTRUE\tFALSE\tFALSE\n"
- ]
- },
- "execution_count": 2,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {p,q,IMPL,KONT,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &\n",
" IMPL=bool(p=TRUE => q=TRUE) &\n",
@@ -987,32 +984,9 @@
},
{
"cell_type": "code",
- "execution_count": 72,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|p|q|F1|F2|\n",
- "|---|---|---|---|\n",
- "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
- ],
- "text/plain": [
- "p\tq\tF1\tF2\n",
- "FALSE\tFALSE\tTRUE\tTRUE\n",
- "FALSE\tTRUE\tFALSE\tTRUE\n",
- "TRUE\tFALSE\tFALSE\tFALSE\n",
- "TRUE\tTRUE\tTRUE\tTRUE\n"
- ]
- },
- "execution_count": 72,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)}"
]
@@ -1054,7 +1028,15 @@
"* X sagt: ```Y ist ein Ritter```\n",
"* Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```\n",
"\n",
- "Können wir bestimmen ob X und Y Ritter oder Schurken sind?\n",
+ "Können wir bestimmen ob X und Y Ritter oder Schurken sind?\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Lösen des Puzzles\n",
+ "\n",
"\n",
"Schritt 1: was sind die Aussagen?\n",
"* $X$: die Person X ist ein Ritter\n",
@@ -1067,37 +1049,14 @@
" * Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```\n",
"\n",
"\n",
- "Schritt 3: Bestimmung der Modelle:\n"
+ "Schritt 3: Bestimmung der Modelle:"
]
},
{
"cell_type": "code",
- "execution_count": 45,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|x|y|S1|S2|Puzzle|\n",
- "|---|---|---|---|---|\n",
- "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
- ],
- "text/plain": [
- "x\ty\tS1\tS2\tPuzzle\n",
- "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\n",
- "FALSE\tTRUE\tFALSE\tTRUE\tFALSE\n",
- "TRUE\tFALSE\tFALSE\tFALSE\tFALSE\n",
- "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\n"
- ]
- },
- "execution_count": 45,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
" S1=bool(x=TRUE ⇔ y=TRUE) &\n",
@@ -1122,32 +1081,9 @@
},
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|x|y|S1|S2|Puzzle|\n",
- "|---|---|---|---|---|\n",
- "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
- ],
- "text/plain": [
- "x\ty\tS1\tS2\tPuzzle\n",
- "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\n",
- "FALSE\tTRUE\tTRUE\tTRUE\tTRUE\n",
- "TRUE\tFALSE\tFALSE\tTRUE\tFALSE\n",
- "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\n"
- ]
- },
- "execution_count": 46,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
" S1=bool(x=TRUE ⇒ y=TRUE) &\n",
@@ -1178,7 +1114,13 @@
"* $\\Longleftrightarrow$ alle Modelle von $\\phi$ sind auch Modelle von $\\psi$ (per Definition von $\\models$)\n",
"* $\\Longleftrightarrow$ in allen Modellen von $\\phi$ hat $\\neg \\psi$ den Wahrheitswert falsch (per Definition von $\\neg$)\n",
"* $\\Longleftrightarrow$ alle Modelle von $\\phi$ sind kein Modell von $\\phi \\wedge \\neg \\psi$ (per Definition von $\\wedge$)\n",
- "* $\\Longleftrightarrow$ $\\phi \\wedge \\neg \\psi$ hat kein Modell (da auch kein Modell von $\\neg \\phi$ ein Modell von $\\phi \\wedge \\neg \\psi$ sein kann)\n",
+ "* $\\Longleftrightarrow$ $\\phi \\wedge \\neg \\psi$ hat kein Modell (da auch kein Modell von $\\neg \\phi$ ein Modell von $\\phi \\wedge \\neg \\psi$ sein kann)\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"Anwendung auf unser Puzzle:\n",
"* Sei $\\phi$ = $(\\mathit{X} \\Leftrightarrow \\mathit{Y}) \\wedge (\\mathit{Y} \\Leftrightarrow (\\mathit{X} \\Leftrightarrow \\neg (\\mathit{Y})))$\n",
@@ -1189,32 +1131,9 @@
},
{
"cell_type": "code",
- "execution_count": 49,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|x|y|S1|S2|Puzzle|WS|\n",
- "|---|---|---|---|---|---|\n",
- "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
- ],
- "text/plain": [
- "x\ty\tS1\tS2\tPuzzle\tWS\n",
- "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\tFALSE\n",
- "FALSE\tTRUE\tFALSE\tTRUE\tFALSE\tFALSE\n",
- "TRUE\tFALSE\tFALSE\tFALSE\tFALSE\tFALSE\n",
- "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\tFALSE\n"
- ]
- },
- "execution_count": 49,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL & \n",
" S1=bool(x=TRUE ⇔ y=TRUE) &\n",
@@ -1244,7 +1163,14 @@
"Wir haben per Transitivität von $\\equiv$, dass $\\phi_1 \\equiv \\phi_k$.\n",
"Da $\\equiv$ auch kommutativ ist, gilt der Beweis auch in die andere Richtung: $\\phi_k \\equiv \\phi_1$.\n",
"Wir haben sowohl $\\phi_1 \\models \\phi_k$ als auch $\\phi_k \\models \\phi_1$.\n",
- " \n",
+ " "
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
"Als kleines Beispiel beweisen wir, dass $\\neg b \\Rightarrow a \\equiv a \\vee b$:\n",
"* $\\neg b \\Rightarrow a$\n",
"* $\\Longleftrightarrow$ $\\neg \\neg b \\vee a$ (Regel: $\\phi \\Rightarrow \\psi \\equiv \\neg \\phi \\vee \\psi$)\n",
@@ -1271,6 +1197,13 @@
"Wir haben per Transitiviät von $\\models$, dass $\\phi_1 \\models \\phi_k$.\n",
"Aber im Gegensatz zum Äquivalenzbeweis gilt hier generell nicht $\\phi_k \\models phi_1$!\n",
"Dieser Beweis kann nicht umgekehrt werden.\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"Wir illustrieren dies Art der Beweisführung mit einem anderen kleinen Puzzle von unserer Insel der Ritter und Schurken:\n",
"* A sagt: ``B ist ein Ritter''\n",
@@ -1280,7 +1213,7 @@
"* $\\neg B$ (nach der zweiten Aussage $B \\Leftrightarrow FALSE$ muss B ein Schurke sein)\n",
"* $\\neg A$ (nach der ersten Aussage $A \\Leftrightarrow B$ muss A demnach auch ein Schurke sein)\n",
"\n",
- "Wir haben per Transitiviät, dass $\\phi_1 \\models \\neg A$, d.h. es folgt aus dem Puzzle, dass A ein Schurke ist.\n"
+ "Wir haben per Transitiviät, dass $\\phi_1 \\models \\neg A$, d.h. es folgt aus dem Puzzle, dass A ein Schurke ist."
]
},
{
@@ -1288,14 +1221,17 @@
"metadata": {},
"source": [
"# Aristoteles: Anfänge der Logik\n",
- "Syllogistik, einer Vorform der Prädikatenlogik\n",
- "* Alle Menschen sind sterblich.\n",
- "* Einige Menschen sind sterblich.\n",
- "* Alle Menschen sind unsterblich.\n",
- "* Einige Menschen sind unsterblich.\n",
"\n",
- "Zusammenhang unter der Annahme, daß es mindestens einen Mensch gibt.\n",
- "(In die Aussagenlogik sind alle vier Aussagen unabhängig.)"
+ "Die [Syllogistik](https://de.wikipedia.org/wiki/Syllogismus), einer Vorform der Prädikatenlogik, geht auf Aristoteles zurück.\n",
+ "\n",
+ "\n",
+ "Was ist der Zusammenhang zwischen folgenden vier Aussagen, unter der Annahme, daß es mindestens einen Mensch gibt?\n",
+ "(In die Aussagenlogik sind alle vier Aussagen unabhängig.)\n",
+ "\n",
+ "1. Alle Menschen sind sterblich.\n",
+ "2. Einige Menschen sind sterblich.\n",
+ "3. Alle Menschen sind unsterblich.\n",
+ "4. Einige Menschen sind unsterblich.\n"
]
},
{
@@ -1309,7 +1245,13 @@
"* <b>Konstanten</b> und <b>Variablen</b> die Objekte darstellen,\n",
"* <b>Funktionen</b> die Objekte auf Objekte abbilden,\n",
"* <b>Prädikate</b> die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden,\n",
- "* <b>Quantoren</b> mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert\n",
+ "* <b>Quantoren</b> mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"Erläuterung:\n",
"* ```2+2 < 5``` ist eine Aussage\n",
@@ -1325,36 +1267,9 @@
},
{
"cell_type": "code",
- "execution_count": 74,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|x|y|res|\n",
- "|---|---|---|\n",
- "|$1$|$1$|$\\mathit{FALSE}$|\n",
- "|$1$|$2$|$\\mathit{TRUE}$|\n",
- "|$1$|$3$|$\\mathit{TRUE}$|\n",
- "|$2$|$1$|$\\mathit{FALSE}$|\n",
- "|$2$|$2$|$\\mathit{FALSE}$|\n",
- "|$2$|$3$|$\\mathit{TRUE}$|\n"
- ],
- "text/plain": [
- "x\ty\tres\n",
- "1\t1\tFALSE\n",
- "1\t2\tTRUE\n",
- "1\t3\tTRUE\n",
- "2\t1\tFALSE\n",
- "2\t2\tFALSE\n",
- "2\t3\tTRUE\n"
- ]
- },
- "execution_count": 74,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {x,y,res | x:1..2 & y:1..3 & res=bool(x<y)}"
]
@@ -1398,23 +1313,9 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\mathit{TRUE}$"
- ],
- "text/plain": [
- "TRUE"
- ]
- },
- "execution_count": 34,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"∃x.(x<5)"
]
@@ -1428,87 +1329,27 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\mathit{TRUE}$\n",
- "\n",
- "**Solution:**\n",
- "* $\\mathit{x} = 0$"
- ],
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = 0"
- ]
- },
- "execution_count": 33,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"x<5"
]
},
{
"cell_type": "code",
- "execution_count": 50,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\mathit{TRUE}$\n",
- "\n",
- "**Solution:**\n",
- "* $\\mathit{x} = 10$"
- ],
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = 10"
- ]
- },
- "execution_count": 50,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"x+20 = 30"
]
},
{
"cell_type": "code",
- "execution_count": 53,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\mathit{TRUE}$\n",
- "\n",
- "**Solution:**\n",
- "* $\\mathit{x} = -100$"
- ],
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = −100"
- ]
- },
- "execution_count": 53,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"x*x = 10000"
]
@@ -1526,7 +1367,14 @@
" \n",
"* Eine Formel $\\psi$ ist eine <b>logische Schlussfolgerung</b> von $\\phi$, wenn alle Modelle von $\\phi$ auch Modelle von $\\psi$ sind.\n",
" * Wir schreiben dies als $\\phi \\models \\psi$.\n",
- " \n",
+ " "
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
"Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:\n",
"\n",
"* eine Menge an Objekten muss ausgewählt werden\n",
@@ -1554,20 +1402,19 @@
" * Beispiel: $\\forall x. (\\forall y. (x \\leq y \\vee x>y)) \\equiv \\forall y. (\\forall x. (x \\leq y \\vee x>y))$\n",
"\n",
"* $\\exists x.( \\exists y. P) \\equiv \\exists y.( \\exists x. P)$\n",
- " * Beispiel: $\\exists x. (\\exists y. (x+y=0)) \\equiv \\exists y. (\\exists x. (x+y=0))$\n",
+ " * Beispiel: $\\exists x. (\\exists y. (x+y=0)) \\equiv \\exists y. (\\exists x. (x+y=0))$\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"Aber Achtung:\n",
"* $\\forall x.( \\exists y. P) \\not\\equiv \\exists y.( \\forall x. P)$\n",
" * Beispiel: $\\forall x. (\\exists y. (y > x)) \\not\\equiv \\exists y. (\\forall x. (y > x)$"
]
},
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
- },
{
"cell_type": "markdown",
"metadata": {},
@@ -1590,6 +1437,13 @@
"* Stellwerkprüfung (Prover Technologies, ...)\n",
"* Datenvalidierung (ProB bei Siemens, Alstom, Thales; Paris L1)\n",
"* Software Entwicklung (AtelierB, Paris L14, L1, ....: seit 1999 kein einziger Bug !)\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"# Andere Logiken\n",
" \n",
@@ -1608,7 +1462,13 @@
"* es gibt Intuitionistische Logik: Beweis durch Widerspruch dort nicht erlaubt\n",
"* es gibt dreiwertige Logiken ( $2/0=1 \\wedge 1=2$ )\n",
"* es gibt die Fuzzy Logik, modale Logiken, temporale Logiken,...\n",
- "* nicht-monotone Logiken\n",
+ "* nicht-monotone Logiken"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
"\n",
"# Zusammenfassung Logik\n",
" \n",