diff --git a/notebooks/presentations/Prolog50_2022.ipynb b/notebooks/presentations/Prolog50_2022.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..7717adaff251d9f1945455a8346adcc2f12385b3
--- /dev/null
+++ b/notebooks/presentations/Prolog50_2022.ipynb
@@ -0,0 +1,284 @@
+{
+ "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",
+ ""
+ ]
+ },
+ {
+ "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",
+ "\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
+}
diff --git a/notebooks/presentations/img/SendMoreMoney.png b/notebooks/presentations/img/SendMoreMoney.png
new file mode 100644
index 0000000000000000000000000000000000000000..4618631d14b2f2af11ab7a4f4874084f1fdef206
Binary files /dev/null and b/notebooks/presentations/img/SendMoreMoney.png differ