diff --git a/notebooks/presentations/BvsLP.ipynb b/notebooks/presentations/BvsLP.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..80ab79828c44b9427b01d19d87647155aec21d1c
--- /dev/null
+++ b/notebooks/presentations/BvsLP.ipynb
@@ -0,0 +1,385 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# B compared to Logic Programming"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Append in B\n",
+ "\n",
+ "The logic program\n",
+ "```\n",
+ "append([],L,L) <-\n",
+ "append([H|X],Y,[H|Z]) <- append(X,Y,Z)\n",
+ "```\n",
+ "can be encoded in various ways in B.\n",
+ "\n",
+ "### Built-in Sequence Operator\n",
+ "\n",
+ "B has built-in sequences, which are special cases of functions, which are special cases of relations, which are sets of pairs.\n",
+ "\n",
+ "The sequence [4,5,6] is represented by the relation {(1,4),(2,5),(3,6)}:\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "[4,5,6] = {(1,4),(2,5),(3,6)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The built-in concatenation operator can be used to append sequences:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$[1,2,3,4,5,6]$"
+ ],
+ "text/plain": [
+ "[1,2,3,4,5,6]"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "[1,2,3] ^ [4,5,6]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = [4,5,6]$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = [4,5,6]"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "[1,2,3] ^ x = [1,2,3,4,5,6]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|x|y|\n",
+ "|---|---|\n",
+ "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$|$[1,2,3]$|\n",
+ "|$\\{(1\\mapsto 1)\\}$|$\\{(1\\mapsto 2),(2\\mapsto 3)\\}$|\n",
+ "|$\\{(1\\mapsto 1),(2\\mapsto 2)\\}$|$\\{(1\\mapsto 3)\\}$|\n",
+ "|$[1,2,3]$|$\\emptyset$|\n"
+ ],
+ "text/plain": [
+ "x\ty\n",
+ "{}\t[1,2,3]\n",
+ "{(1|->1)}\t{(1|->2),(2|->3)}\n",
+ "{(1|->1),(2|->2)}\t{(1|->3)}\n",
+ "[1,2,3]\t{}\n"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x,y | x^y = [1,2,3]}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "One can also write the append as a B function. Note that B is strongly typed (and user defined functions cannot yet be polymorphic), hence we have to provide the type for the arguments to the function."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{app} = \\lambda(\\mathit{x},\\mathit{y})\\qdot(\\mathit{x} \\in \\mathit{seq}(\\mathit{INTEGER}) \\land \\mathit{y} \\in \\mathit{seq}(\\mathit{INTEGER})\\mid \\mathit{x} \\bunion \\{\\mathit{i},\\mathit{e}\\mid \\mathit{i} - \\mathit{size}(\\mathit{x}) \\mapsto \\mathit{e} \\in \\mathit{y}\\})$\n",
+ "* $\\mathit{res} = [1,2,3,4]$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tapp = λ(x,y)·(x ∈ seq(INTEGER) ∧ y ∈ seq(INTEGER)∣x ∪ {i,e∣i − size(x) ↦ e ∈ y})\n",
+ "\tres = [1,2,3,4]"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "app = %(x,y).(x:seq(INTEGER) & y:seq(INTEGER) | x \\/ {i,e | (i-size(x),e) : y}) & app([1,2],[3,4]) = res"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Recursion using transitive closure\n",
+ "\n",
+ "Given an operator TP from sets to sets, one can compute the transitive closure\n",
+ "using ```closure(TP)```. Together with the relational image operator ```.[.]``` one can\n",
+ "compute the least fixed point containing a starting set S \n",
+ "(given the well known conditions) using ```closure(TP)[S]```.\n",
+ "\n",
+ "To simplify the presentation, we encode a variation of append, working on sets:\n",
+ "```\n",
+ "set_app({},L,L) <-\n",
+ "set_app({H}\\/X],Y,{H}\\/Z) <- set_app(X,Y,Z)\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{LHM} = \\{((\\emptyset\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\emptyset\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\}),((\\{\\mathit{FALSE}\\}\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\{\\mathit{FALSE}\\}\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{FALSE},\\mathit{TRUE}\\}\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{FALSE},\\mathit{TRUE}\\}\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{TRUE}\\}\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{TRUE}\\}\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\})\\}$\n",
+ "* $\\mathit{HB} = ((\\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\})) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}))$\n",
+ "* $\\mathit{tp} = \\{\\mathit{S},\\mathit{TPS}\\mid \\mathit{S} \\in ((\\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\})) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\})) \\land \\exists(\\mathit{x},\\mathit{y},\\mathit{z},\\mathit{h})\\qdot(\\mathit{x} \\mapsto \\mathit{y} \\mapsto \\mathit{z} = \\mathit{S} \\land \\mathit{h} \\in \\{\\mathit{FALSE},\\mathit{TRUE}\\} \\land \\mathit{TPS} = (\\mathit{x} \\bunion \\{\\mathit{h}\\}) \\mapsto \\mathit{y} \\mapsto (\\mathit{z} \\bunion \\{\\mathit{h}\\}))\\}$\n",
+ "* $\\mathit{TYPE} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$\n",
+ "* $\\mathit{Facts} = \\{((\\emptyset\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\emptyset\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tLHM = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE}),(({FALSE}↦{FALSE})↦{FALSE}),(({FALSE}↦{TRUE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{FALSE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{TRUE})↦{FALSE,TRUE}),(({TRUE}↦{FALSE})↦{FALSE,TRUE}),(({TRUE}↦{TRUE})↦{TRUE})}\n",
+ "\tHB = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))\n",
+ "\ttp = {S,TPS∣S ∈ ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE})) ∧ ∃(x,y,z,h)·(x ↦ y ↦ z = S ∧ h ∈ {FALSE,TRUE} ∧ TPS = (x ∪ {h}) ↦ y ↦ (z ∪ {h}))}\n",
+ "\tTYPE = {FALSE,TRUE}\n",
+ "\tFacts = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE})}"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)\n",
+ "&\n",
+ "Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts\n",
+ "&\n",
+ "tp = /*@symbolic*/ {S,TPS|S:HB & #(x,y,z,h).( (x,y,z) = S & h:TYPE & TPS= (x\\/{h},y,z\\/{h}))} // The TP Operator\n",
+ "&\n",
+ "LHM = closure(tp)[Facts] // the least Herbrand model"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Axiomatic Encoding using logical implication\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{Model} = \\{((\\emptyset\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\}),((\\emptyset\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\{\\mathit{FALSE}\\}\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{TRUE}\\}\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\}),((\\{\\mathit{FALSE}\\}\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\{\\mathit{TRUE}\\}\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{FALSE},\\mathit{TRUE}\\}\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\}),((\\{\\mathit{FALSE},\\mathit{TRUE}\\}\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE},\\mathit{TRUE}\\})\\}$\n",
+ "* $\\mathit{HB} = ((\\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\})) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}))$\n",
+ "* $\\mathit{TYPE} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$\n",
+ "* $\\mathit{Facts} = \\{((\\emptyset\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\emptyset\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tModel = {((∅↦{TRUE})↦{TRUE}),((∅↦{FALSE})↦{FALSE}),(({FALSE}↦{TRUE})↦{FALSE,TRUE}),(({TRUE}↦{TRUE})↦{TRUE}),(({FALSE}↦{FALSE})↦{FALSE}),(({TRUE}↦{FALSE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{TRUE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{FALSE})↦{FALSE,TRUE})}\n",
+ "\tHB = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))\n",
+ "\tTYPE = {FALSE,TRUE}\n",
+ "\tFacts = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE})}"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)\n",
+ "&\n",
+ "Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts\n",
+ "&\n",
+ "Facts <: Model\n",
+ "&\n",
+ "!(x,y,z).( (x,y,z):Model => !h.(h:TYPE => (x\\/{h},y,z\\/{h}):Model))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{Model} = ((\\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\})) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}))$\n",
+ "* $\\mathit{HB} = ((\\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\})) * \\pow(\\{\\mathit{FALSE},\\mathit{TRUE}\\}))$\n",
+ "* $\\mathit{TYPE} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$\n",
+ "* $\\mathit{Facts} = \\{((\\emptyset\\mapsto\\{\\mathit{FALSE}\\})\\mapsto\\{\\mathit{FALSE}\\}),((\\emptyset\\mapsto\\{\\mathit{TRUE}\\})\\mapsto\\{\\mathit{TRUE}\\})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tModel = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))\n",
+ "\tHB = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))\n",
+ "\tTYPE = {FALSE,TRUE}\n",
+ "\tFacts = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE})}"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)\n",
+ "&\n",
+ "Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts\n",
+ "&\n",
+ "Facts <: Model\n",
+ "&\n",
+ "!(x,y,z).( (x,y,z):Model => !h.(h:TYPE => (x\\/{h},y,z\\/{h}):Model))\n",
+ "&\n",
+ "Model = HB"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{time\\_out}$"
+ ],
+ "text/plain": [
+ "time_out"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)\n",
+ "&\n",
+ "Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts\n",
+ "&\n",
+ "AllModels = {Model | Facts <: Model &\n",
+ " !(x,y,z).( (x,y,z):Model => !h.(h:TYPE => (x\\/{h},y,z\\/{h}):Model))}"
+ ]
+ },
+ {
+ "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"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}