From eb8242252fd8bb4710140289d9b5a8b342bb50f3 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Fri, 11 May 2018 11:28:49 +0200
Subject: [PATCH] update example notebook
---
notebooks/tutorials/prob_solver_intro.ipynb | 68 ++++++++++++++++++---
1 file changed, 58 insertions(+), 10 deletions(-)
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 2a3ea5c..3a7c066 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/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,
--
GitLab