From 7b04452b5bd888c0a9978ff052e58a6aa3a69dd1 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Mon, 16 Jul 2018 10:01:05 +0200
Subject: [PATCH] update notebook

---
 notebooks/tutorials/prob_solver_intro.ipynb | 233 ++++++++++++++++++--
 1 file changed, 212 insertions(+), 21 deletions(-)

diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 72bd4c8..85b339b 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -18,8 +18,11 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$5070602400912917605986812821504$"
+      ],
       "text/plain": [
-       "1024"
+       "5070602400912917605986812821504"
       ]
      },
      "execution_count": 1,
@@ -28,7 +31,7 @@
     }
    ],
    "source": [
-    "2**10"
+    "2**102"
    ]
   },
   {
@@ -45,6 +48,9 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$1267650600228229401496703205376$"
+      ],
       "text/plain": [
        "1267650600228229401496703205376"
       ]
@@ -73,6 +79,9 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$"
+      ],
       "text/plain": [
        "TRUE"
       ]
@@ -101,6 +110,12 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $x = -10$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -132,6 +147,9 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$\\{-10,10\\}$"
+      ],
       "text/plain": [
        "{−10,10}"
       ]
@@ -160,6 +178,19 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $R = 8$\n",
+       "* $S = 9$\n",
+       "* $D = 7$\n",
+       "* $E = 5$\n",
+       "* $Y = 2$\n",
+       "* $M = 1$\n",
+       "* $N = 6$\n",
+       "* $O = 0$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -202,6 +233,19 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $R = 0$\n",
+       "* $S = 9$\n",
+       "* $D = 0$\n",
+       "* $E = 0$\n",
+       "* $Y = 0$\n",
+       "* $M = 1$\n",
+       "* $N = 0$\n",
+       "* $O = 0$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -243,6 +287,9 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$\\{(((((((9\\mapsto 5)\\mapsto 6)\\mapsto 7)\\mapsto 1)\\mapsto 0)\\mapsto 8)\\mapsto 2)\\}$"
+      ],
       "text/plain": [
        "{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}"
       ]
@@ -276,6 +323,18 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $P = 4$\n",
+       "* $A = 1$\n",
+       "* $S = 3$\n",
+       "* $I = 0$\n",
+       "* $K = 2$\n",
+       "* $N = 9$\n",
+       "* $O = 8$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -317,6 +376,13 @@
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $queens = \\{(1\\mapsto 1),(2\\mapsto 5),(3\\mapsto 8),(4\\mapsto 6),(5\\mapsto 3),(6\\mapsto 7),(7\\mapsto 2),(8\\mapsto 4)\\}$\n",
+       "* $n = 8$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -340,7 +406,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 11,
    "metadata": {},
    "outputs": [
     {
@@ -369,7 +435,7 @@
        "8\t8\t4\n"
       ]
      },
-     "execution_count": 1,
+     "execution_count": 11,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -380,11 +446,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 12,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $queens = \\{(1\\mapsto 1),(2\\mapsto 3),(3\\mapsto 5),(4\\mapsto 13),(5\\mapsto 11),(6\\mapsto 4),(7\\mapsto 15),(8\\mapsto 7),(9\\mapsto 16),(10\\mapsto 14),(11\\mapsto 2),(12\\mapsto 8),(13\\mapsto 6),(14\\mapsto 9),(15\\mapsto 12),(16\\mapsto 10)\\}$\n",
+       "* $n = 16$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -393,7 +466,7 @@
        "\tn = 16"
       ]
      },
-     "execution_count": 11,
+     "execution_count": 12,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -426,11 +499,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 13,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $A = TRUE$\n",
+       "* $B = TRUE$\n",
+       "* $C = FALSE$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -440,7 +521,7 @@
        "\tC = FALSE"
       ]
      },
-     "execution_count": 12,
+     "execution_count": 13,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -460,16 +541,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 14,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$\\{((TRUE\\mapsto TRUE)\\mapsto FALSE)\\}$"
+      ],
       "text/plain": [
        "{((TRUE↦TRUE)↦FALSE)}"
       ]
      },
-     "execution_count": 13,
+     "execution_count": 14,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -480,6 +564,33 @@
     "        (B=TRUE <=> A=TRUE) }"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|Nr|A|B|C|\n",
+       "|---|---|---|---|\n",
+       "|1|TRUE|TRUE|FALSE|\n"
+      ],
+      "text/plain": [
+       "Nr\tA\tB\tC\n",
+       "1\tTRUE\tTRUE\tFALSE\n"
+      ]
+     },
+     "execution_count": 20,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table {A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &\n",
+    "        (B=TRUE <=> A=TRUE) }"
+   ]
+  },
   {
    "cell_type": "markdown",
    "metadata": {},
@@ -489,11 +600,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 15,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $DOM = (1 \\ldots 9)$\n",
+       "* $Board = \\{(1\\mapsto\\{(1\\mapsto 7),(2\\mapsto 8),(3\\mapsto 1),(4\\mapsto 6),(5\\mapsto 3),(6\\mapsto 2),(7\\mapsto 9),(8\\mapsto 4),(9\\mapsto 5)\\}),(2\\mapsto\\{(1\\mapsto 9),(2\\mapsto 5),(3\\mapsto 2),(4\\mapsto 7),(5\\mapsto 1),(6\\mapsto 4),(7\\mapsto 6),(8\\mapsto 3),(9\\mapsto 8)\\}),(3\\mapsto\\{(1\\mapsto 4),(2\\mapsto 3),(3\\mapsto 6),(4\\mapsto 8),(5\\mapsto 9),(6\\mapsto 5),(7\\mapsto 7),(8\\mapsto 1),(9\\mapsto 2)\\}),(4\\mapsto\\{(1\\mapsto 2),(2\\mapsto 4),(3\\mapsto 9),(4\\mapsto 3),(5\\mapsto 7),(6\\mapsto 6),(7\\mapsto 8),(8\\mapsto 5),(9\\mapsto 1)\\}),(5\\mapsto\\{(1\\mapsto 6),(2\\mapsto 7),(3\\mapsto 3),(4\\mapsto 5),(5\\mapsto 8),(6\\mapsto 1),(7\\mapsto 2),(8\\mapsto 9),(9\\mapsto 4)\\}),(6\\mapsto\\{(1\\mapsto 5),(2\\mapsto 1),(3\\mapsto 8),(4\\mapsto 4),(5\\mapsto 2),(6\\mapsto 9),(7\\mapsto 3),(8\\mapsto 6),(9\\mapsto 7)\\}),(7\\mapsto\\{(1\\mapsto 1),(2\\mapsto 9),(3\\mapsto 4),(4\\mapsto 2),(5\\mapsto 6),(6\\mapsto 7),(7\\mapsto 5),(8\\mapsto 8),(9\\mapsto 3)\\}),(8\\mapsto\\{(1\\mapsto 8),(2\\mapsto 6),(3\\mapsto 7),(4\\mapsto 1),(5\\mapsto 5),(6\\mapsto 3),(7\\mapsto 4),(8\\mapsto 2),(9\\mapsto 9)\\}),(9\\mapsto\\{(1\\mapsto 3),(2\\mapsto 2),(3\\mapsto 5),(4\\mapsto 9),(5\\mapsto 4),(6\\mapsto 8),(7\\mapsto 1),(8\\mapsto 7),(9\\mapsto 6)\\})\\}$\n",
+       "* $SUBSQ = \\{\\{1,2,3\\},\\{4,5,6\\},\\{7,8,9\\}\\}$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -503,7 +622,7 @@
        "\tSUBSQ = {{1,2,3},{4,5,6},{7,8,9}}"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 15,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -554,11 +673,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 16,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $stolen = \\{(16\\mapsto 2),(17\\mapsto 4),(23\\mapsto 0),(24\\mapsto 0),(39\\mapsto 0),(40\\mapsto 0)\\}$\n",
+       "* $coins = \\{16,17,23,24,39,40\\}$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -567,7 +693,7 @@
        "\tcoins = {16,17,23,24,39,40}"
       ]
      },
-     "execution_count": 15,
+     "execution_count": 16,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -587,11 +713,21 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 17,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $Persons = \\{\"Agatha\",\"Charles\",\"butler\"\\}$\n",
+       "* $richer = \\{(\"Agatha\"\\mapsto\"Charles\"),(\"butler\"\\mapsto\"Agatha\"),(\"butler\"\\mapsto\"Charles\")\\}$\n",
+       "* $victim = \"Agatha\"$\n",
+       "* $killer = \"Agatha\"$\n",
+       "* $hates = \\{(\"Agatha\"\\mapsto\"Agatha\"),(\"Agatha\"\\mapsto\"Charles\"),(\"Charles\"\\mapsto\"butler\"),(\"butler\"\\mapsto\"Agatha\"),(\"butler\"\\mapsto\"Charles\")\\}$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -603,7 +739,7 @@
        "\thates = {(\"Agatha\"↦\"Agatha\"),(\"Agatha\"↦\"Charles\"),(\"Charles\"↦\"butler\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")}"
       ]
      },
-     "execution_count": 16,
+     "execution_count": 17,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -639,11 +775,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 18,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $a = \\{(1\\mapsto 0),(2\\mapsto 2),(3\\mapsto 6),(4\\mapsto 9),(5\\mapsto 14),(6\\mapsto 24),(7\\mapsto 25)\\}$\n",
+       "* $len = 25$\n",
+       "* $n = 7$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -653,7 +797,7 @@
        "\tn = 7"
       ]
      },
-     "execution_count": 17,
+     "execution_count": 18,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -674,11 +818,27 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 19,
    "metadata": {},
    "outputs": [
     {
      "data": {
+      "text/markdown": [
+       "$TRUE$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $n1 = \"a\"$\n",
+       "* $iso = \\{(1\\mapsto\"c\"),(2\\mapsto\"a\"),(3\\mapsto\"b\")\\}$\n",
+       "* $n2 = \"b\"$\n",
+       "* $n3 = \"c\"$\n",
+       "* $V = \\{1,2,3\\}$\n",
+       "* $g1 = \\{(1\\mapsto 2),(1\\mapsto 3),(2\\mapsto 3)\\}$\n",
+       "* $g2 = \\{(\"a\"\\mapsto\"b\"),(\"c\"\\mapsto\"a\"),(\"c\"\\mapsto\"b\")\\}$\n",
+       "* $v1 = 1$\n",
+       "* $v2 = 2$\n",
+       "* $v3 = 3$\n",
+       "* $N = \\{\"a\",\"b\",\"c\"\\}$"
+      ],
       "text/plain": [
        "TRUE\n",
        "\n",
@@ -696,7 +856,7 @@
        "\tN = {\"a\",\"b\",\"c\"}"
       ]
      },
-     "execution_count": 18,
+     "execution_count": 19,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -711,6 +871,36 @@
     "iso: V >->> N & !v.(v:V => iso[g1[{v}]] = g2[iso[{v}]])\n",
     "END"
    ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 21,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\"abc\"$"
+      ],
+      "text/plain": [
+       "\"abc\""
+      ]
+     },
+     "execution_count": 21,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "\"abc\""
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
   }
  ],
  "metadata": {
@@ -720,8 +910,9 @@
    "name": "prob2"
   },
   "language_info": {
+   "codemirror_mode": "prob2_jupyter_repl",
    "file_extension": ".prob",
-   "mimetype": "text/x-prob",
+   "mimetype": "text/x-prob2-jupyter-repl",
    "name": "prob"
   }
  },
-- 
GitLab