update example notebook

notebooks/tutorials/prob_solver_intro.ipynb

@@ -4,7 +4,11 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "We can use ProB to perform computations:"
+    "# Introduction to ProB's constraint solving capabilities\n",
+    "We can use ProB to perform computations:\n",
+    "\n",
+    "## Expressions\n",
+    "Expressions in B have a value. With ProB and with ProB's Jupyter backend, you can evaluate expresssions such as:"
    ]
   },
   {
@@ -58,7 +62,36 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "We can find solutions for equations. Open variables are implicitly existentially quantified:"
+    "## Predicates\n",
+    "ProB can also be used to evaluate predicates (B distinguishes between expressions which have a value and predicates which are either true or false)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "2+2>3"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Within predicates you can use **open** variables, which are implicitly existentially quantified.\n",
+    "ProB will display the solution for the open variables, if possible."
    ]
   },
   {
@@ -85,7 +118,8 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "We can find all solutions to a predicate by using the set comprehension notation."
+    "We can find all solutions to a predicate by using the set comprehension notation.\n",
+    "Note that by this we turn a predicate into an expression."
    ]
   },
   {
@@ -112,6 +146,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
+    "## Send More Money Puzzle\n",
     "We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:"
    ]
   },
@@ -207,6 +242,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
+    "## KISS PASSION Puzzle\n",
     "A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem."
    ]
   },
@@ -238,6 +274,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
+    "## N-Queens Puzzle\n",
     "Here is how we can solve the famous N-Queens puzzle for n=8."
    ]
   },
@@ -293,15 +330,18 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "A Puzzle from Smullyan:\n",
-    " Knights: always tell the truth\n",
-    " Knaves: always lie\n",
+    "## Knights and Knave Puzzle\n",
+    "Here is a puzzle from Smullyan involving an island with only knights and knaves.\n",
+    "We know that:\n",
+    " - Knights: always tell the truth\n",
+    " - Knaves: always lie\n",
     "\n",
-    " 1: A says: “B is a knave or C is a knave”\n",
-    " 2: B says “A is a knight”\n",
+    "We are given the following information about three persons A,B,C on the island:\n",
+    " 1. A says: “B is a knave or C is a knave”\n",
+    " 2. B says “A is a knight”\n",
     "\n",
-    " What are A & B & C?\n",
-    " Note: A,B,C are equal to TRUE if they are a knight and FALSE if they are a knave."
+    "What are A, B and C?\n",
+    "Note: we model A,B,C as boolean variables which are equal to TRUE if they are a knight and FALSE if they are a knave."
    ]
   },
   {
@@ -325,6 +365,14 @@
     " (B=TRUE <=> A=TRUE) // Sentence 2"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Note that in B there are no propositional variables: A,B and C are expressions with a value.\n",
+    "To turn them into a predicate we need to use the comparison with TRUE."
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 15,