add another notebook

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

notebooks/presentations/Prolog50_2022.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {
+    "slideshow": {
+     "slide_type": "slide"
+    }
+   },
+   "source": [
+    "# ProB's Prolog Constraint Solver\n",
+    "## Demo using Jupyter\n",
+    "\n",
+    "### Prolog Day 2022\n",
+    "\n",
+    "https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel\n",
+    "\n",
+    "![ProB](./img/prob_logo.png)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {
+    "slideshow": {
+     "slide_type": "subslide"
+    }
+   },
+   "source": [
+    "We highlight some of the features of ProB's constraint solving kernel written in Prolog,\n",
+    "dealing with unbounded arithmetic, higher-order and possibly infinite sets:"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {
+    "slideshow": {
+     "slide_type": "slide"
+    }
+   },
+   "source": [
+    "# Some Features"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {
+    "slideshow": {
+     "slide_type": "subslide"
+    }
+   },
+   "source": [
+    "Automatically detecting infinite sets:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "scrolled": false,
+    "vscode": {
+     "languageId": "classicalb"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "Primes = {x|x>1 & !y.(y:2..x-1 => x mod y >0)}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Generating some prime > 100 and using Unicode notation:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Primes = {x∣x>1 ∧ ∀y.(y∈2..x-1⇒ x mod y>0)} ∧\n",
+    "some_prime ∈ Primes & some_prime > 100"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Getting first 100 primes by intersection:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "scrolled": true,
+    "vscode": {
+     "languageId": "python"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "1..100 ∩ {x∣x>1∧∀y.(y∈2..x-1⇒ x mod y>0)}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Getting first 1000 primes; observe that P1000 is computed explicitly while Primes is automatically kept symbolic:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "P1000 = 1..1000 ∩ Primes ∧\n",
+    "Primes = {x∣x>1 ∧ ∀y.(y∈2..x-1⇒ x mod y>0)}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {
+    "slideshow": {
+     "slide_type": "subslide"
+    }
+   },
+   "source": [
+    "Solving the famous SEND+MORE = MONEY Puzzle with\n",
+    "multiline input:\n",
+    "\n",
+    "<div>\n",
+    "<img src=\"./img/SendMoreMoney.png\" width=\"400\"/>\n",
+    "</div>\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "vscode": {
+     "languageId": "python"
+    }
+   },
+   "outputs": [],
+   "source": [
+    ":table {S,E,N,D,M,O,R,Y |\n",
+    "\n",
+    "{S, E, N, D, M, O, R, Y} ⊆ 0..9\n",
+    "∧ S > 0 ∧ M > 0\n",
+    "∧ card({S, E, N, D, M, O, R, Y}) = 8\n",
+    "∧\n",
+    "            S*1000 + E*100 + N*10 + D\n",
+    "+           M*1000 + O*100 + R*10 + E\n",
+    "= M*10000 + O*1000 + N*100 + E*10 + Y\n",
+    "\n",
+    "}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Find distinct digits such that this multiplication becomes true:\n",
+    "\n",
+    "![ProB](./img/KissKissPassion.png)\n",
+    "\n",
+    "(This is a more difficult version of the Send+More=Money puzzle.)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "vscode": {
+     "languageId": "python"
+    }
+   },
+   "outputs": [],
+   "source": [
+    ":table {K,I,S,P,A,O,N | {K,P} ⊆ 1..9 ∧\n",
+    "    {I,S,A,O,N} ⊆ 0..9 ∧\n",
+    "    (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) \n",
+    "     =  1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N ∧\n",
+    "    card({K, I, S, P, A, O, N}) = 7}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {
+    "slideshow": {
+     "slide_type": "subslide"
+    }
+   },
+   "source": [
+    "## Visualisation\n",
+    "\n",
+    "In B, sequences are also functions, functions are relations, and relations are sets.\n",
+    "Relations can be displayed visually:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "vscode": {
+     "languageId": "python"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "{x,y | x∈1..5 ∧ y∈1..5 ∧ x>y}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "slideshow": {
+     "slide_type": "subslide"
+    },
+    "vscode": {
+     "languageId": "python"
+    }
+   },
+   "outputs": [],
+   "source": [
+    ":pref DOT_ENGINE=circo"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "vscode": {
+     "languageId": "python"
+    }
+   },
+   "outputs": [],
+   "source": [
+    ":dot expr_as_graph (\"K5\", {x,y | x∈1..5 ∧ y∈1..5 ∧ x>y})"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    ":dot expr_as_graph (\"K6\", {x,y | x∈1..6 ∧ y∈1..6 ∧ x>y})"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "codemirror_mode": "prob2_jupyter_repl",
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob2-jupyter-repl",
+   "name": "prob"
+  },
+  "vscode": {
+   "interpreter": {
+    "hash": "301501caf4ced90c88b4867a75dc974b7f77d88824feb914d0cf4e75e12213b3"
+   }
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}