diff --git a/notebooks/presentations/BvsLP.ipynb b/notebooks/presentations/BvsLP.ipynb
index 80ab79828c44b9427b01d19d87647155aec21d1c..4fde7f527b08ac1b49d1b021bbaa08176ae260ea 100644
--- a/notebooks/presentations/BvsLP.ipynb
+++ b/notebooks/presentations/BvsLP.ipynb
@@ -4,7 +4,18 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "# B compared to Logic Programming"
+ "# B compared to Logic Programming\n",
+ "\n",
+ "\n",
+ "Important differences:\n",
+ "* B is based on classical predicate logic with classical negation\n",
+ "* B is based on arithmetic and set theory, LP on (rational) trees aka uninterpreted functions\n",
+ "* B is strongly typed, but allows higher-order data types\n",
+ "* B allows arbitrary nesting of quantifiers and negation\n",
+ "\n",
+ "As B is based on classical negation and classical predicate logic (without induction), how can it deal with natural numbers, transitive closure, ...?\n",
+ "* Integer arithmetic is built-in, providing induction through the back door. One can construct bijections between user-defined sets and the integers or natural numbers.\n",
+ "* Transitive closure is built-in, providing another way to introduce induction or recursion.\n"
]
},
{
@@ -50,6 +61,89 @@
"[4,5,6] = {(1,4),(2,5),(3,6)}"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"216pt\" height=\"134pt\"\n",
+ " viewBox=\"0.00 0.00 216.32 134.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 130)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-130 213.321,-130 213.321,5 -4,5\"/>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-126 0,-126 0,-90 54,-90 54,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>6</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-36 0,-36 0,-0 54,-0 54,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+ "</g>\n",
+ "<!-- 3->6 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>3->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M27,-89.614C27,-77.2403 27,-60.3686 27,-46.2198\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"30.5001,-46.0504 27,-36.0504 23.5001,-46.0504 30.5001,-46.0504\"/>\n",
+ "<text text-anchor=\"middle\" x=\"45.6606\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">[4,5,6]</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"126,-126 72,-126 72,-90 126,-90 126,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node6\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"126,-36 72,-36 72,-0 126,-0 126,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 2->5 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>2->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M99,-89.614C99,-77.2403 99,-60.3686 99,-46.2198\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"102.5,-46.0504 99,-36.0504 95.5001,-46.0504 102.5,-46.0504\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117.661\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">[4,5,6]</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node7\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"198,-126 144,-126 144,-90 198,-90 198,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"171\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node9\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"198,-36 144,-36 144,-0 198,-0 198,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"171\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 1->4 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>1->4</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M171,-89.614C171,-77.2403 171,-60.3686 171,-46.2198\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"174.5,-46.0504 171,-36.0504 167.5,-46.0504 174.5,-46.0504\"/>\n",
+ "<text text-anchor=\"middle\" x=\"189.661\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">[4,5,6]</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [[4,5,6]]>"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph [4,5,6]"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -331,6 +425,13 @@
"Model = HB"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Additional Material"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 35,
diff --git a/notebooks/presentations/LPOP18.ipynb b/notebooks/presentations/LPOP18.ipynb
index 6fd4bae5f2f7a8d6cf4c14b6bc88f7b5a0a5d237..2df8badc77a9d29498a684968179e7c03192f978 100644
--- a/notebooks/presentations/LPOP18.ipynb
+++ b/notebooks/presentations/LPOP18.ipynb
@@ -3141,17 +3141,17 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\mathit{TRUE}$\n",
+ "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{inf} = \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\}$\n",
- "* $\\mathit{res} = ((900 \\ldots 1100) \\binter \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\})$"
+ "* $\\mathit{res} = ((900 \\upto 1100) \\binter \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\})$"
],
"text/plain": [
"TRUE\n",
@@ -3161,7 +3161,7 @@
"\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})"
]
},
- "execution_count": 40,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -3363,16 +3363,16 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "Execution time: 0.266020568 seconds"
+ "Execution time: 0.716030873 seconds"
],
"text/plain": [
- "Execution time: 0.266020568 seconds"
+ "Execution time: 0.716030873 seconds"
]
},
"metadata": {},
@@ -3384,22 +3384,22 @@
"$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $\\mathit{s3} = \\exists 500\\in\\{20,40,\\0xpto,9980,10000\\}$\n",
+ "* $\\mathit{s3} = \\#500\\in\\{20,40,\\ldots,9980,10000\\}$\n",
"* $\\mathit{n} = 4$\n",
- "* $\\mathit{s1} = \\exists 2500\\in\\{4,8,\\0xpto,9996,10000\\}$\n",
- "* $\\mathit{s2} = \\exists 2000\\in\\{5,10,\\0xpto,9995,10000\\}$"
+ "* $\\mathit{s1} = \\#2500\\in\\{4,8,\\ldots,9996,10000\\}$\n",
+ "* $\\mathit{s2} = \\#2000\\in\\{5,10,\\ldots,9995,10000\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
- "\ts3 = ∃500∈{20,40,…,9980,10000}\n",
+ "\ts3 = #500∈{20,40,…,9980,10000}\n",
"\tn = 4\n",
- "\ts1 = ∃2500∈{4,8,…,9996,10000}\n",
- "\ts2 = ∃2000∈{5,10,…,9995,10000}"
+ "\ts1 = #2500∈{4,8,…,9996,10000}\n",
+ "\ts2 = #2000∈{5,10,…,9995,10000}"
]
},
- "execution_count": 42,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -3421,16 +3421,16 @@
},
{
"cell_type": "code",
- "execution_count": 88,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "Execution time: 0.014582494 seconds"
+ "Execution time: 0.122529996 seconds"
],
"text/plain": [
- "Execution time: 0.014582494 seconds"
+ "Execution time: 0.122529996 seconds"
]
},
"metadata": {},
@@ -3439,13 +3439,13 @@
{
"data": {
"text/markdown": [
- "$TRUE$\n",
+ "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $xy = \\exists201\\in\\{1,2,\\0xpto,299,300\\}$\n",
- "* $x = (1 \\ldots 100)$\n",
- "* $y = (200 \\ldots 300)$\n",
- "* $n = 100$"
+ "* $\\mathit{xy} = \\exists 201\\in\\{1,2,\\ldots,299,300\\}$\n",
+ "* $\\mathit{x} = (1 \\upto 100)$\n",
+ "* $\\mathit{y} = (200 \\upto 300)$\n",
+ "* $\\mathit{n} = 100$"
],
"text/plain": [
"TRUE\n",
@@ -3457,7 +3457,7 @@
"\tn = 100"
]
},
- "execution_count": 88,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -3490,16 +3490,16 @@
},
{
"cell_type": "code",
- "execution_count": 90,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "Execution time: 0.546787958 seconds"
+ "Execution time: 2.035079877 seconds"
],
"text/plain": [
- "Execution time: 0.546787958 seconds"
+ "Execution time: 2.035079877 seconds"
]
},
"metadata": {},
@@ -3508,13 +3508,13 @@
{
"data": {
"text/markdown": [
- "$TRUE$\n",
+ "$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $xy = \\{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,\\0xpto\\}$\n",
- "* $x = \\{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64\\}$\n",
- "* $y = \\{200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256\\}$\n",
- "* $n = 100$"
+ "* $\\mathit{xy} = \\{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,\\ldots\\}$\n",
+ "* $\\mathit{x} = \\{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64\\}$\n",
+ "* $\\mathit{y} = \\{200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256\\}$\n",
+ "* $\\mathit{n} = 100$"
],
"text/plain": [
"TRUE\n",
@@ -3526,7 +3526,7 @@
"\tn = 100"
]
},
- "execution_count": 90,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -3645,7 +3645,7 @@
},
{
"cell_type": "code",
- "execution_count": 65,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -3675,7 +3675,7 @@
"\tr1 = 317"
]
},
- "execution_count": 65,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -3769,7 +3769,9 @@
" - works well for animation, data validation, disproving\n",
" - limitations appear for symbolic model checking (IC3,...)\n",
" - Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable) \n",
- " "
+ "- CHR: can complement ProB's default backend\n",
+ " - currently only very limited propagations (>, >=, x=y+c, ...)\n",
+ " - very difficult to control and avoid propagation loops"
]
},
{
@@ -4420,6 +4422,60 @@
" res = SIGNAL \\ nxt[SIGNAL]"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{x} = \\mathbb N \\wedge \\mathit{y} = NAT$"
+ ],
+ "text/plain": [
+ "x = ℕ ∧ y = NAT"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint x=NATURAL & y=NAT"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = \\mathit{NATURAL}$\n",
+ "* $\\mathit{y} = (0 \\upto 3)$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = NATURAL\n",
+ "\ty = (0 ‥ 3)"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x=NATURAL & y=NAT"
+ ]
+ },
{
"cell_type": "code",
"execution_count": null,