diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 1d7bf85f5f534d9fad82f9e2ca327008d2e24b3f..4566d56851b2b92faadc72b49c5b17b04a2c8871 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -366,10 +366,982 @@
     "?- wff(Formula,\"(p∧(q∨(¬p)))\",\"\")."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "f9005519",
+   "metadata": {},
+   "source": [
+    "The above Prolog term `and(p,or(q,not(p)))` represents the logical formula in tree form.\n",
+    "We can display the tree as a dag (directed acyclic graph) using the following subsidiary code\n",
+    "(in future the Jupyter kernel will probably have a dedicated command to show a term graphically):"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "id": "f6116612",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:subtree/3 were retracted (click to expand)</summary><pre>:- dynamic subtree/3.\n",
+       "\n",
+       "subtree(A, B, C) :-\n",
+       "    A=..[_|D],\n",
+       "    nth1(B, D, C).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:subtree/3 were retracted:\n",
+       ":- dynamic subtree/3.\n",
+       "\n",
+       "subtree(A, B, C) :-\n",
+       "    A=..[_|D],\n",
+       "    nth1(B, D, C).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:subtree/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:rec_subtree/2 were retracted (click to expand)</summary><pre>:- dynamic rec_subtree/2.\n",
+       "\n",
+       "rec_subtree(A, B) :-\n",
+       "    A=B.\n",
+       "rec_subtree(A, B) :-\n",
+       "    subtree(A, _, C),\n",
+       "    rec_subtree(C, B).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:rec_subtree/2 were retracted:\n",
+       ":- dynamic rec_subtree/2.\n",
+       "\n",
+       "rec_subtree(A, B) :-\n",
+       "    A=B.\n",
+       "rec_subtree(A, B) :-\n",
+       "    subtree(A, _, C),\n",
+       "    rec_subtree(C, B).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:rec_subtree/2\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:subnode/3 were retracted (click to expand)</summary><pre>:- dynamic subnode/3.\n",
+       "\n",
+       "subnode(A, [shape/B, label/C], D) :-\n",
+       "    rec_subtree(D, A),\n",
+       "    functor(A, C, _),\n",
+       "    (   atom(A)\n",
+       "    ->  B=egg\n",
+       "    ;   number(A)\n",
+       "    ->  B=oval\n",
+       "    ;   B=rect\n",
+       "    ).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:subnode/3 were retracted:\n",
+       ":- dynamic subnode/3.\n",
+       "\n",
+       "subnode(A, [shape/B, label/C], D) :-\n",
+       "    rec_subtree(D, A),\n",
+       "    functor(A, C, _),\n",
+       "    (   atom(A)\n",
+       "    ->  B=egg\n",
+       "    ;   number(A)\n",
+       "    ->  B=oval\n",
+       "    ;   B=rect\n",
+       "    ).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:subnode/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "subtree(Term,Nr,SubTerm) :- \n",
+    "   Term =.. [_|ArgList], %obtain arguments of the term\n",
+    "   nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number\n",
+    "\n",
+    "% recursive and transitive closure of subtree\n",
+    "rec_subtree(Term,Sub) :- Term = Sub.\n",
+    "rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub).\n",
+    "\n",
+    "subnode(Sub,[shape/S, label/F],Formula) :- \n",
+    "   rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering\n",
+    "   functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "id": "d7e68593",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "Node | Dot | \n",
+       ":- | :- | \n",
+       "and(p,or(q,not(p))) | [shape/rect,label/and] | \n",
+       "p | [shape/egg,label/p] | \n",
+       "or(q,not(p)) | [shape/rect,label/or] | \n",
+       "q | [shape/egg,label/q] | \n",
+       "not(p) | [shape/rect,label/not] | \n",
+       "p | [shape/egg,label/p] | "
+      ],
+      "text/plain": [
+       "Node | Dot | \n",
+       ":- | :- | \n",
+       "and(p,or(q,not(p))) | [shape/rect,label/and] | \n",
+       "p | [shape/egg,label/p] | \n",
+       "or(q,not(p)) | [shape/rect,label/or] | \n",
+       "q | [shape/egg,label/q] | \n",
+       "not(p) | [shape/rect,label/not] | \n",
+       "p | [shape/egg,label/p] | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p)))))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "id": "3646e3ee",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "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 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"70.68,-87.05 72.46,-87.15 74.22,-87.3 75.95,-87.49 77.65,-87.74 79.31,-88.03 80.92,-88.36 82.48,-88.75 83.99,-89.18 85.43,-89.65 86.8,-90.16 88.1,-90.71 89.32,-91.31 90.45,-91.94 91.51,-92.61 92.47,-93.31 93.35,-94.04 94.13,-94.8 94.81,-95.59 95.41,-96.41 95.91,-97.25 96.31,-98.11 96.62,-98.99 96.83,-99.89 96.96,-100.8 96.99,-101.72 96.93,-102.65 96.79,-103.59 96.57,-104.53 96.27,-105.47 95.89,-106.41 95.44,-107.35 94.92,-108.28 94.33,-109.2 93.69,-110.11 92.98,-111.01 92.22,-111.89 91.41,-112.75 90.56,-113.59 89.67,-114.41 88.73,-115.2 87.76,-115.96 86.76,-116.69 85.74,-117.39 84.68,-118.06 83.61,-118.69 82.52,-119.29 81.41,-119.84 80.28,-120.35 79.14,-120.82 77.99,-121.25 76.84,-121.64 75.67,-121.97 74.5,-122.26 73.33,-122.51 72.15,-122.7 70.96,-122.85 69.78,-122.95 68.59,-123 67.41,-123 66.22,-122.95 65.04,-122.85 63.85,-122.7 62.67,-122.51 61.5,-122.26 60.33,-121.97 59.16,-121.64 58.01,-121.25 56.86,-120.82 55.72,-120.35 54.59,-119.84 53.48,-119.29 52.39,-118.69 51.32,-118.06 50.26,-117.39 49.24,-116.69 48.24,-115.96 47.27,-115.2 46.33,-114.41 45.44,-113.59 44.59,-112.75 43.78,-111.89 43.02,-111.01 42.31,-110.11 41.67,-109.2 41.08,-108.28 40.56,-107.35 40.11,-106.41 39.73,-105.47 39.43,-104.53 39.21,-103.59 39.07,-102.65 39.01,-101.72 39.04,-100.8 39.17,-99.89 39.38,-98.99 39.69,-98.11 40.09,-97.25 40.59,-96.41 41.19,-95.59 41.87,-94.8 42.65,-94.04 43.53,-93.31 44.49,-92.61 45.55,-91.94 46.68,-91.31 47.9,-90.71 49.2,-90.16 50.57,-89.65 52.01,-89.18 53.52,-88.75 55.08,-88.36 56.69,-88.03 58.35,-87.74 60.05,-87.49 61.78,-87.3 63.54,-87.15 65.32,-87.05 67.1,-87 68.9,-87 70.68,-87.05\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)&#45;&gt;p -->\n<g id=\"edge1\" class=\"edge\">\n<title>not(p)&#45;&gt;p</title>\n<path fill=\"none\" stroke=\"black\" d=\"M123.79,-86.8C109.35,-73.17 89.14,-54.07 73.84,-39.62\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"76.01,-36.86 66.34,-32.54 71.21,-41.95 76.01,-36.86\"/>\n<text text-anchor=\"middle\" x=\"105.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- and(p,or(q,not(p))) -->\n<g id=\"node4\" class=\"node\">\n<title>and(p,or(q,not(p)))</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"54,-297 0,-297 0,-261 54,-261 54,-297\"/>\n<text text-anchor=\"middle\" x=\"27\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">and</text>\n</g>\n<!-- and(p,or(q,not(p)))&#45;&gt;p -->\n<g id=\"edge2\" class=\"edge\">\n<title>and(p,or(q,not(p)))&#45;&gt;p</title>\n<path fill=\"none\" stroke=\"black\" d=\"M25.59,-260.99C23.18,-227.43 19.48,-150.47 30,-87 32.35,-72.85 37.06,-57.61 41.53,-45.15\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"44.94,-46.02 45.16,-35.42 38.38,-43.57 44.94,-46.02\"/>\n<text text-anchor=\"middle\" x=\"28.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- or(q,not(p)) -->\n<g id=\"node5\" class=\"node\">\n<title>or(q,not(p))</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"95,-210 41,-210 41,-174 95,-174 95,-210\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">or</text>\n</g>\n<!-- and(p,or(q,not(p)))&#45;&gt;or(q,not(p)) -->\n<g id=\"edge3\" class=\"edge\">\n<title>and(p,or(q,not(p)))&#45;&gt;or(q,not(p))</title>\n<path fill=\"none\" stroke=\"black\" d=\"M35.3,-260.8C41.02,-248.93 48.74,-232.93 55.24,-219.45\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"58.52,-220.7 59.72,-210.18 52.22,-217.66 58.52,-220.7\"/>\n<text text-anchor=\"middle\" x=\"52.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n<!-- or(q,not(p))&#45;&gt;q -->\n<g id=\"edge4\" class=\"edge\">\n<title>or(q,not(p))&#45;&gt;q</title>\n<path fill=\"none\" stroke=\"black\" d=\"M68,-173.8C68,-162.16 68,-146.55 68,-133.24\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"71.5,-133.18 68,-123.18 64.5,-133.18 71.5,-133.18\"/>\n<text text-anchor=\"middle\" x=\"71.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- or(q,not(p))&#45;&gt;not(p) -->\n<g id=\"edge5\" class=\"edge\">\n<title>or(q,not(p))&#45;&gt;not(p)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M82.98,-173.8C93.71,-161.47 108.33,-144.68 120.33,-130.89\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"123.12,-133.02 127.05,-123.18 117.84,-128.42 123.12,-133.02\"/>\n<text text-anchor=\"middle\" x=\"112.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n</g>\n</svg>\n",
+      "text/plain": [
+       "digraph {\n",
+       "\"p\" [shape=\"egg\", label=\"p\"]\n",
+       "\"q\" [shape=\"egg\", label=\"q\"]\n",
+       "\"not(p)\" [shape=\"rect\", label=\"not\"]\n",
+       "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\"]\n",
+       "\"or(q,not(p))\" [shape=\"rect\", label=\"or\"]\n",
+       "    \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+       "    \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+       "    \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+       "    \"or(q,not(p))\" -> \"q\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+       "    \"or(q,not(p))\" -> \"not(p)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+       "}"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "11b3a8ad",
+   "metadata": {},
+   "source": [
+    "Below we will study how one can assign a truth-value to logical formulas like the one above.\n",
+    "\n",
+    "## Truth tables\n",
+    "\n",
+    "Every logical connective has a truth-table, indicating how it maps the truth of its arguments to its own truth value.\n",
+    "For example, `and` maps inputs `true` and `false` to `false`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 21,
+   "id": "350b9756",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:not/2 were retracted (click to expand)</summary><pre>:- dynamic not/2.\n",
+       "\n",
+       "not(true, false).\n",
+       "not(false, true).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:not/2 were retracted:\n",
+       ":- dynamic not/2.\n",
+       "\n",
+       "not(true, false).\n",
+       "not(false, true).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:not/2\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:and/3 were retracted (click to expand)</summary><pre>:- dynamic and/3.\n",
+       "\n",
+       "and(true, A, A).\n",
+       "and(false, _, false).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:and/3 were retracted:\n",
+       ":- dynamic and/3.\n",
+       "\n",
+       "and(true, A, A).\n",
+       "and(false, _, false).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:and/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:or/3 were retracted (click to expand)</summary><pre>:- dynamic or/3.\n",
+       "\n",
+       "or(true, _, true).\n",
+       "or(false, A, A).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:or/3 were retracted:\n",
+       ":- dynamic or/3.\n",
+       "\n",
+       "or(true, _, true).\n",
+       "or(false, A, A).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:or/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:implies/3 were retracted (click to expand)</summary><pre>:- dynamic implies/3.\n",
+       "\n",
+       "implies(A, B, C) :-\n",
+       "    not(A, D),\n",
+       "    or(D, B, C).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:implies/3 were retracted:\n",
+       ":- dynamic implies/3.\n",
+       "\n",
+       "implies(A, B, C) :-\n",
+       "    not(A, D),\n",
+       "    or(D, B, C).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:implies/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:equiv/3 were retracted (click to expand)</summary><pre>:- dynamic equiv/3.\n",
+       "\n",
+       "equiv(A, B, C) :-\n",
+       "    implies(A, B, D),\n",
+       "    implies(B, A, E),\n",
+       "    and(D, E, C).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:equiv/3 were retracted:\n",
+       ":- dynamic equiv/3.\n",
+       "\n",
+       "equiv(A, B, C) :-\n",
+       "    implies(A, B, D),\n",
+       "    implies(B, A, E),\n",
+       "    and(D, E, C).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:equiv/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:truth_value/1 were retracted (click to expand)</summary><pre>:- dynamic truth_value/1.\n",
+       "\n",
+       "truth_value(true).\n",
+       "truth_value(false).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:truth_value/1 were retracted:\n",
+       ":- dynamic truth_value/1.\n",
+       "\n",
+       "truth_value(true).\n",
+       "truth_value(false).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:truth_value/1\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:truth_table/7 were retracted (click to expand)</summary><pre>:- dynamic truth_table/7.\n",
+       "\n",
+       "truth_table(A, B, C, D, E, F, G) :-\n",
+       "    truth_value(A),\n",
+       "    truth_value(B),\n",
+       "    not(A, C),\n",
+       "    and(A, B, D),\n",
+       "    or(A, B, E),\n",
+       "    implies(A, B, F),\n",
+       "    equiv(A, B, G).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:truth_table/7 were retracted:\n",
+       ":- dynamic truth_table/7.\n",
+       "\n",
+       "truth_table(A, B, C, D, E, F, G) :-\n",
+       "    truth_value(A),\n",
+       "    truth_value(B),\n",
+       "    not(A, C),\n",
+       "    and(A, B, D),\n",
+       "    or(A, B, E),\n",
+       "    implies(A, B, F),\n",
+       "    equiv(A, B, G).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:truth_table/7\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "not(true,false).\n",
+    "not(false,true).\n",
+    "\n",
+    "and(true,V,V) :- truth_value(V).\n",
+    "and(false,_,false).\n",
+    "\n",
+    "or(true,_,true).\n",
+    "or(false,V,V) :- truth_value(V).\n",
+    "\n",
+    "implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res).\n",
+    "equiv(A,B,Res) :- implies(A,B,AiB), implies(B,A,BiA), and(AiB,BiA,Res).\n",
+    "\n",
+    "truth_value(true).\n",
+    "truth_value(false).\n",
+    "\n",
+    "truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :- \n",
+    "   truth_value(A), truth_value(B),\n",
+    "   not(A,NotA), and(A,B,AandB), or(A,B,AorB),\n",
+    "   implies(A,B,AiB), equiv(A,B,AeB)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 22,
+   "id": "54b57ff8",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "A | B | NotA | AandB | AorB | AimpliesB | AequivB | \n",
+       ":- | :- | :- | :- | :- | :- | :- | \n",
+       "true | true | false | true | true | true | true | \n",
+       "true | false | false | false | true | false | false | \n",
+       "false | true | true | false | true | true | false | \n",
+       "false | false | true | false | false | true | true | "
+      ],
+      "text/plain": [
+       "A | B | NotA | AandB | AorB | AimpliesB | AequivB | \n",
+       ":- | :- | :- | :- | :- | :- | :- | \n",
+       "true | true | false | true | true | true | true | \n",
+       "true | false | false | false | true | false | false | \n",
+       "false | true | true | false | true | true | false | \n",
+       "false | false | true | false | false | true | true | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 23,
+   "id": "175c00d0",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:value/3 were retracted (click to expand)</summary><pre>:- dynamic value/3.\n",
+       "\n",
+       "value(A, B, C) :-\n",
+       "    atomic(A),\n",
+       "    member(A/C, B).\n",
+       "value(and(A, B), C, D) :-\n",
+       "    value(A, C, E),\n",
+       "    value(B, C, F),\n",
+       "    and(E, F, D).\n",
+       "value(or(A, B), C, D) :-\n",
+       "    value(A, C, E),\n",
+       "    value(B, C, F),\n",
+       "    or(E, F, D).\n",
+       "value(not(A), B, C) :-\n",
+       "    value(A, B, D),\n",
+       "    not(D, C).\n",
+       "value(implies(A, B), C, D) :-\n",
+       "    value(or(not(A), B), C, D).\n",
+       "value(equiv(A, B), C, D) :-\n",
+       "    value(and(implies(A, B), implies(B, A)),\n",
+       "          C,\n",
+       "          D).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:value/3 were retracted:\n",
+       ":- dynamic value/3.\n",
+       "\n",
+       "value(A, B, C) :-\n",
+       "    atomic(A),\n",
+       "    member(A/C, B).\n",
+       "value(and(A, B), C, D) :-\n",
+       "    value(A, C, E),\n",
+       "    value(B, C, F),\n",
+       "    and(E, F, D).\n",
+       "value(or(A, B), C, D) :-\n",
+       "    value(A, C, E),\n",
+       "    value(B, C, F),\n",
+       "    or(E, F, D).\n",
+       "value(not(A), B, C) :-\n",
+       "    value(A, B, D),\n",
+       "    not(D, C).\n",
+       "value(implies(A, B), C, D) :-\n",
+       "    value(or(not(A), B), C, D).\n",
+       "value(equiv(A, B), C, D) :-\n",
+       "    value(and(implies(A, B), implies(B, A)),\n",
+       "          C,\n",
+       "          D).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:value/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "value(X,Interpretation,Value) :- \n",
+    "   atomic(X), % we could also use: proposition(X),\n",
+    "   member(X/Value,Interpretation).\n",
+    "value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),\n",
+    "   and(VA,VB,Val).\n",
+    "value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),\n",
+    "   or(VA,VB,Val).\n",
+    "value(not(A),I,Val) :- value(A,I,VA),\n",
+    "   not(VA,Val).\n",
+    "value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val).\n",
+    "value(equiv(A,B),I,Val) :- \n",
+    "   value(and(implies(A,B),implies(B,A)),I,Val).\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "id": "eee17774",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mRes = false"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- value(and(p,or(q,not(p))), [p/true, q/false],Res)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "id": "78473da0",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "true | false | false | \n",
+       "false | true | false | \n",
+       "false | false | false | "
+      ],
+      "text/plain": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "true | false | false | \n",
+       "false | true | false | \n",
+       "false | false | false | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 35,
+   "id": "2ee60c15",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:subnode_val/4 were retracted (click to expand)</summary><pre>:- dynamic subnode_val/4.\n",
+       "\n",
+       "subnode_val(A, [shape/B, label/C, style/filled, fillcolor/D], E, F) :-\n",
+       "    rec_subtree(E, A),\n",
+       "    functor(A, C, _),\n",
+       "    (   atom(A)\n",
+       "    ->  B=egg\n",
+       "    ;   number(A)\n",
+       "    ->  B=oval\n",
+       "    ;   B=rect\n",
+       "    ),\n",
+       "    (   value(A, F, true)\n",
+       "    ->  D=olive\n",
+       "    ;   D=salmon1\n",
+       "    ).\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:subnode_val/4 were retracted:\n",
+       ":- dynamic subnode_val/4.\n",
+       "\n",
+       "subnode_val(A, [shape/B, label/C, style/filled, fillcolor/D], E, F) :-\n",
+       "    rec_subtree(E, A),\n",
+       "    functor(A, C, _),\n",
+       "    (   atom(A)\n",
+       "    ->  B=egg\n",
+       "    ;   number(A)\n",
+       "    ->  B=oval\n",
+       "    ;   B=rect\n",
+       "    ),\n",
+       "    (   value(A, F, true)\n",
+       "    ->  D=olive\n",
+       "    ;   D=salmon1\n",
+       "    ).\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:subnode_val/4\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "\n",
+    "subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :- \n",
+    "   rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering\n",
+    "   functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),\n",
+    "   (value(Sub,Interpretation,true) -> C=olive ; C=sienna1)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 36,
+   "id": "2b497dad",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "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 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"70.68,-87.05 72.46,-87.15 74.22,-87.3 75.95,-87.49 77.65,-87.74 79.31,-88.03 80.92,-88.36 82.48,-88.75 83.99,-89.18 85.43,-89.65 86.8,-90.16 88.1,-90.71 89.32,-91.31 90.45,-91.94 91.51,-92.61 92.47,-93.31 93.35,-94.04 94.13,-94.8 94.81,-95.59 95.41,-96.41 95.91,-97.25 96.31,-98.11 96.62,-98.99 96.83,-99.89 96.96,-100.8 96.99,-101.72 96.93,-102.65 96.79,-103.59 96.57,-104.53 96.27,-105.47 95.89,-106.41 95.44,-107.35 94.92,-108.28 94.33,-109.2 93.69,-110.11 92.98,-111.01 92.22,-111.89 91.41,-112.75 90.56,-113.59 89.67,-114.41 88.73,-115.2 87.76,-115.96 86.76,-116.69 85.74,-117.39 84.68,-118.06 83.61,-118.69 82.52,-119.29 81.41,-119.84 80.28,-120.35 79.14,-120.82 77.99,-121.25 76.84,-121.64 75.67,-121.97 74.5,-122.26 73.33,-122.51 72.15,-122.7 70.96,-122.85 69.78,-122.95 68.59,-123 67.41,-123 66.22,-122.95 65.04,-122.85 63.85,-122.7 62.67,-122.51 61.5,-122.26 60.33,-121.97 59.16,-121.64 58.01,-121.25 56.86,-120.82 55.72,-120.35 54.59,-119.84 53.48,-119.29 52.39,-118.69 51.32,-118.06 50.26,-117.39 49.24,-116.69 48.24,-115.96 47.27,-115.2 46.33,-114.41 45.44,-113.59 44.59,-112.75 43.78,-111.89 43.02,-111.01 42.31,-110.11 41.67,-109.2 41.08,-108.28 40.56,-107.35 40.11,-106.41 39.73,-105.47 39.43,-104.53 39.21,-103.59 39.07,-102.65 39.01,-101.72 39.04,-100.8 39.17,-99.89 39.38,-98.99 39.69,-98.11 40.09,-97.25 40.59,-96.41 41.19,-95.59 41.87,-94.8 42.65,-94.04 43.53,-93.31 44.49,-92.61 45.55,-91.94 46.68,-91.31 47.9,-90.71 49.2,-90.16 50.57,-89.65 52.01,-89.18 53.52,-88.75 55.08,-88.36 56.69,-88.03 58.35,-87.74 60.05,-87.49 61.78,-87.3 63.54,-87.15 65.32,-87.05 67.1,-87 68.9,-87 70.68,-87.05\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)&#45;&gt;p -->\n<g id=\"edge1\" class=\"edge\">\n<title>not(p)&#45;&gt;p</title>\n<path fill=\"none\" stroke=\"black\" d=\"M123.79,-86.8C109.35,-73.17 89.14,-54.07 73.84,-39.62\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"76.01,-36.86 66.34,-32.54 71.21,-41.95 76.01,-36.86\"/>\n<text text-anchor=\"middle\" x=\"105.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- and(p,or(q,not(p))) -->\n<g id=\"node4\" class=\"node\">\n<title>and(p,or(q,not(p)))</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"54,-297 0,-297 0,-261 54,-261 54,-297\"/>\n<text text-anchor=\"middle\" x=\"27\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">and</text>\n</g>\n<!-- and(p,or(q,not(p)))&#45;&gt;p -->\n<g id=\"edge2\" class=\"edge\">\n<title>and(p,or(q,not(p)))&#45;&gt;p</title>\n<path fill=\"none\" stroke=\"black\" d=\"M25.59,-260.99C23.18,-227.43 19.48,-150.47 30,-87 32.35,-72.85 37.06,-57.61 41.53,-45.15\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"44.94,-46.02 45.16,-35.42 38.38,-43.57 44.94,-46.02\"/>\n<text text-anchor=\"middle\" x=\"28.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- or(q,not(p)) -->\n<g id=\"node5\" class=\"node\">\n<title>or(q,not(p))</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"95,-210 41,-210 41,-174 95,-174 95,-210\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">or</text>\n</g>\n<!-- and(p,or(q,not(p)))&#45;&gt;or(q,not(p)) -->\n<g id=\"edge3\" class=\"edge\">\n<title>and(p,or(q,not(p)))&#45;&gt;or(q,not(p))</title>\n<path fill=\"none\" stroke=\"black\" d=\"M35.3,-260.8C41.02,-248.93 48.74,-232.93 55.24,-219.45\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"58.52,-220.7 59.72,-210.18 52.22,-217.66 58.52,-220.7\"/>\n<text text-anchor=\"middle\" x=\"52.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n<!-- or(q,not(p))&#45;&gt;q -->\n<g id=\"edge4\" class=\"edge\">\n<title>or(q,not(p))&#45;&gt;q</title>\n<path fill=\"none\" stroke=\"black\" d=\"M68,-173.8C68,-162.16 68,-146.55 68,-133.24\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"71.5,-133.18 68,-123.18 64.5,-133.18 71.5,-133.18\"/>\n<text text-anchor=\"middle\" x=\"71.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- or(q,not(p))&#45;&gt;not(p) -->\n<g id=\"edge5\" class=\"edge\">\n<title>or(q,not(p))&#45;&gt;not(p)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M82.98,-173.8C93.71,-161.47 108.33,-144.68 120.33,-130.89\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"123.12,-133.02 127.05,-123.18 117.84,-128.42 123.12,-133.02\"/>\n<text text-anchor=\"middle\" x=\"112.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n</g>\n</svg>\n",
+      "text/plain": [
+       "digraph {\n",
+       "\"p\" [shape=\"egg\", label=\"p\", style=\"filled\", fillcolor=\"olive\"]\n",
+       "\"q\" [shape=\"egg\", label=\"q\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+       "\"not(p)\" [shape=\"rect\", label=\"not\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+       "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+       "\"or(q,not(p))\" [shape=\"rect\", label=\"or\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+       "    \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+       "    \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+       "    \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+       "    \"or(q,not(p))\" -> \"q\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+       "    \"or(q,not(p))\" -> \"not(p)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+       "}"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3)"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "f6116612",
+   "id": "0fd23f05",
    "metadata": {
     "vscode": {
      "languageId": "prolog"