diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 86be5b9682b7e6d1e63f20639671a9a2b4ad2cd6..bc92d88edeac5896b870e6fe82e09b07788162bf 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -60,13 +60,23 @@
"wff --> \"(\", wff, \"∧\", wff, \")\".\n",
"wff --> \"(\", wff, \"∨\", wff, \")\".\n",
"wff --> \"(\", wff, \"→\", wff, \")\".\n",
- "wff --> \"(\", wff, \"⟺\", wff, \")\"."
+ "wff --> \"(\", wff, \"⟺\", wff, \")\".\n",
+ "\n",
+ "is_wff(String) :- wff(String,\"\")."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "87125415",
+ "metadata": {},
+ "source": [
+ "In Prolog string literals can be written using double quotes. Such literals are actually syntactic sugar for list of ASCII/Unicode numbers. (In most Prolog systems this is the default; in SWI Prolog you need to set the Prolog flag double_quotes to the value codes; see above)."
]
},
{
"cell_type": "code",
"execution_count": 2,
- "id": "fc6823ad",
+ "id": "3d91dfdc",
"metadata": {
"vscode": {
"languageId": "prolog"
@@ -76,7 +86,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mtrue"
+ "\u001b[1mX = [112,32,32,32,32,113]"
]
},
"metadata": {},
@@ -84,13 +94,21 @@
}
],
"source": [
- "?- wff(\"p\",\"\")."
+ "?- X=\"p q\"."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "15b8ea6b",
+ "metadata": {},
+ "source": [
+ "We can use the above grammar and check whether a string is a well-formed formula:"
]
},
{
"cell_type": "code",
"execution_count": 3,
- "id": "152289b6",
+ "id": "fc6823ad",
"metadata": {
"vscode": {
"languageId": "prolog"
@@ -100,7 +118,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mtrue"
+ "\u001b[1;31mfalse"
]
},
"metadata": {},
@@ -108,12 +126,60 @@
}
],
"source": [
- "?- wff(\"(¬p)\",\"\")."
+ "?- is_wff(\"p\")."
]
},
{
"cell_type": "code",
"execution_count": 4,
+ "id": "a7168548",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- is_wff(\"p q\")."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "152289b6",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- is_wff(\"(¬p)\")."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
"id": "2c3dd1bf",
"metadata": {
"vscode": {
@@ -124,7 +190,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mtrue"
+ "\u001b[1;31mfalse"
]
},
"metadata": {},
@@ -132,7 +198,7 @@
}
],
"source": [
- "?- wff(\"(p∧(q∨(¬p)))\",\"\").\n",
+ "?- is_wff(\"(p∧(q∨(¬p)))\").\n",
"%comment."
]
},
@@ -153,7 +219,7 @@
"- ¬ p ∧ ¬ q → ¬ p ∨ ¬ q\n",
"\n",
"We will try not not mix conjunction/disjunction and implication/equivalence without parentheses.\n",
- "We will also not try to improve our Prolog parser here to accomodate these precedences.\n",
+ "We will also not improve our Prolog parser here to accomodate these precedences.\n",
"This is the subject of another course (on compiler construction)."
]
},
@@ -162,13 +228,22 @@
"id": "92b6dc2d",
"metadata": {},
"source": [
- "We will also see much later that Prolog allows one to annotate grammars with semantic values, here to generate\n",
+ "We now want to represent propositional logic formulas as Prolog terms. Simple propostions are translated into Prolog atoms, while for the logical connectives we use Prolog functors like not/1, and/2, ...:\n",
+ "\n",
+ "| Formula | Prolog Term |\n",
+ "| --- | --- | \n",
+ "| p | p |\n",
+ "| (¬p) | not(p) |\n",
+ "| (p ∧ q) | and(p,q) |\n",
+ "| (p ∧ (¬p)) | and(p,not(p)) |\n",
+ "\n",
+ "We can actually generate those Prolog terms from the syntax of the formula using the following piece of Prolog code. Indeed, as we will see much later, Prolog allows one to annotate grammars with semantic values, here to generate\n",
"a Prolog term representing the logical formal in the form of a syntax tree:"
]
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 7,
"id": "78163b60",
"metadata": {
"vscode": {
@@ -191,7 +266,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 8,
"id": "6b9c3364",
"metadata": {
"vscode": {
@@ -215,7 +290,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 9,
"id": "075dc3b2",
"metadata": {
"vscode": {
@@ -239,7 +314,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 10,
"id": "338cb7dd",
"metadata": {
"vscode": {
@@ -250,7 +325,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mFormula = and(p,or(q,not(p)))"
+ "\u001b[1mF = and(p,or(q,not(p)))"
]
},
"metadata": {},
@@ -258,7 +333,7 @@
}
],
"source": [
- "?- parse_wff(\"(p∧(q∨(¬p)))\",Formula)."
+ "?- parse_wff(\"(p∧(q∨(¬p)))\",F)."
]
},
{
@@ -273,7 +348,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 11,
"id": "f6116612",
"metadata": {
"vscode": {
@@ -292,12 +367,13 @@
"\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)."
+ " functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect).\n",
+ "\n"
]
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 12,
"id": "d7e68593",
"metadata": {
"vscode": {
@@ -347,7 +423,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 13,
"id": "3646e3ee",
"metadata": {
"vscode": {
@@ -361,77 +437,177 @@
"<?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",
+ "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\n",
+ " -->\n",
+ "<!-- Pages: 1 -->\n",
+ "<svg width=\"139pt\" height=\"221pt\"\n",
+ " viewBox=\"0.00 0.00 139.49 221.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 217)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-217 135.49,-217 135.49,4 -4,4\"/>\n",
+ "<!-- p -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>p</title>\n",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"105.4,-0.05 107.16,-0.15 108.91,-0.3 110.62,-0.49 112.31,-0.74 113.96,-1.03 115.56,-1.36 117.11,-1.75 118.6,-2.18 120.02,-2.65 121.38,-3.16 122.67,-3.71 123.88,-4.31 125.01,-4.94 126.05,-5.61 127.01,-6.31 127.87,-7.04 128.65,-7.8 129.33,-8.59 129.92,-9.41 130.41,-10.25 130.81,-11.11 131.12,-11.99 131.33,-12.89 131.45,-13.8 131.49,-14.72 131.43,-15.65 131.29,-16.59 131.07,-17.53 130.77,-18.47 130.4,-19.41 129.95,-20.35 129.43,-21.28 128.85,-22.2 128.21,-23.11 127.51,-24.01 126.76,-24.89 125.96,-25.75 125.11,-26.59 124.23,-27.41 123.3,-28.2 122.34,-28.96 121.35,-29.69 120.33,-30.39 119.29,-31.06 118.22,-31.69 117.14,-32.29 116.04,-32.84 114.92,-33.35 113.79,-33.82 112.65,-34.25 111.51,-34.64 110.35,-34.97 109.19,-35.26 108.02,-35.51 106.85,-35.7 105.68,-35.85 104.51,-35.95 103.33,-36 102.16,-36 100.98,-35.95 99.81,-35.85 98.63,-35.7 97.46,-35.51 96.3,-35.26 95.14,-34.97 93.98,-34.64 92.83,-34.25 91.7,-33.82 90.57,-33.35 89.45,-32.84 88.35,-32.29 87.27,-31.69 86.2,-31.06 85.16,-30.39 84.14,-29.69 83.15,-28.96 82.19,-28.2 81.26,-27.41 80.37,-26.59 79.53,-25.75 78.73,-24.89 77.97,-24.01 77.28,-23.11 76.63,-22.2 76.05,-21.28 75.54,-20.35 75.09,-19.41 74.71,-18.47 74.41,-17.53 74.19,-16.59 74.05,-15.65 74,-14.72 74.03,-13.8 74.16,-12.89 74.37,-11.99 74.67,-11.11 75.07,-10.25 75.57,-9.41 76.16,-8.59 76.84,-7.8 77.61,-7.04 78.48,-6.31 79.44,-5.61 80.48,-4.94 81.61,-4.31 82.82,-3.71 84.1,-3.16 85.46,-2.65 86.89,-2.18 88.38,-1.75 89.93,-1.36 91.53,-1.03 93.18,-0.74 94.86,-0.49 96.58,-0.3 98.32,-0.15 100.08,-0.05 101.86,0 103.63,0 105.4,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102.74\" y=\"-12.95\" 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=\"31.4,-88.55 33.16,-88.65 34.91,-88.8 36.62,-88.99 38.31,-89.24 39.96,-89.53 41.56,-89.86 43.11,-90.25 44.6,-90.68 46.02,-91.15 47.38,-91.66 48.67,-92.21 49.88,-92.81 51.01,-93.44 52.05,-94.11 53.01,-94.81 53.87,-95.54 54.65,-96.3 55.33,-97.09 55.92,-97.91 56.41,-98.75 56.81,-99.61 57.12,-100.49 57.33,-101.39 57.45,-102.3 57.49,-103.22 57.43,-104.15 57.29,-105.09 57.07,-106.03 56.77,-106.97 56.4,-107.91 55.95,-108.85 55.43,-109.78 54.85,-110.7 54.21,-111.61 53.51,-112.51 52.76,-113.39 51.96,-114.25 51.11,-115.09 50.23,-115.91 49.3,-116.7 48.34,-117.46 47.35,-118.19 46.33,-118.89 45.29,-119.56 44.22,-120.19 43.14,-120.79 42.04,-121.34 40.92,-121.85 39.79,-122.32 38.65,-122.75 37.51,-123.14 36.35,-123.47 35.19,-123.76 34.02,-124.01 32.85,-124.2 31.68,-124.35 30.51,-124.45 29.33,-124.5 28.16,-124.5 26.98,-124.45 25.81,-124.35 24.63,-124.2 23.46,-124.01 22.3,-123.76 21.14,-123.47 19.98,-123.14 18.83,-122.75 17.7,-122.32 16.57,-121.85 15.45,-121.34 14.35,-120.79 13.27,-120.19 12.2,-119.56 11.16,-118.89 10.14,-118.19 9.15,-117.46 8.19,-116.7 7.26,-115.91 6.37,-115.09 5.53,-114.25 4.73,-113.39 3.97,-112.51 3.28,-111.61 2.63,-110.7 2.05,-109.78 1.54,-108.85 1.09,-107.91 0.71,-106.97 0.41,-106.03 0.19,-105.09 0.05,-104.15 0,-103.22 0.03,-102.3 0.16,-101.39 0.37,-100.49 0.67,-99.61 1.07,-98.75 1.57,-97.91 2.16,-97.09 2.84,-96.3 3.61,-95.54 4.48,-94.81 5.44,-94.11 6.48,-93.44 7.61,-92.81 8.82,-92.21 10.1,-91.66 11.46,-91.15 12.89,-90.68 14.38,-90.25 15.93,-89.86 17.53,-89.53 19.18,-89.24 20.86,-88.99 22.58,-88.8 24.32,-88.65 26.08,-88.55 27.86,-88.5 29.63,-88.5 31.4,-88.55\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.74\" y=\"-101.45\" 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=\"129.74,-124.5 75.74,-124.5 75.74,-88.5 129.74,-88.5 129.74,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102.74\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n",
+ "</g>\n",
+ "<!-- not(p)->p -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>not(p)->p</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M102.74,-88.41C102.74,-76.76 102.74,-61.05 102.74,-47.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"106.24,-47.86 102.74,-37.86 99.24,-47.86 106.24,-47.86\"/>\n",
+ "<text text-anchor=\"middle\" x=\"106.12\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- or(q,not(p)) -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>or(q,not(p))</title>\n",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"70.74,-213 16.74,-213 16.74,-177 70.74,-177 70.74,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43.74\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">or</text>\n",
+ "</g>\n",
+ "<!-- or(q,not(p))->q -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>or(q,not(p))->q</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M40.78,-176.91C38.75,-165.18 36,-149.34 33.64,-135.75\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"37.12,-135.3 31.96,-126.05 30.22,-136.5 37.12,-135.3\"/>\n",
+ "<text text-anchor=\"middle\" x=\"41.12\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- or(q,not(p))->not(p) -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>or(q,not(p))->not(p)</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M55.4,-176.91C63.75,-164.67 75.15,-147.95 84.68,-133.99\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"87.31,-136.33 90.06,-126.1 81.53,-132.39 87.31,-136.33\"/>\n",
+ "<text text-anchor=\"middle\" x=\"81.12\" y=\"-145.7\" 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",
+ "\"or(q,not(p))\" [shape=\"rect\", label=\"or\"]\n",
+ " \"not(p)\" -> \"p\" [label=\"1\", 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(_,_,or(q,not(p))),subtree/3)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "2aacffa9",
+ "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 10.0.1 (20240210.2158)\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",
+ "<svg width=\"177pt\" height=\"310pt\"\n",
+ " viewBox=\"0.00 0.00 177.00 309.50\" 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 305.5)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-305.5 173,-305.5 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",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"54.66,-0.05 56.42,-0.15 58.16,-0.3 59.88,-0.49 61.57,-0.74 63.21,-1.03 64.81,-1.36 66.36,-1.75 67.85,-2.18 69.28,-2.65 70.64,-3.16 71.93,-3.71 73.14,-4.31 74.26,-4.94 75.31,-5.61 76.26,-6.31 77.13,-7.04 77.91,-7.8 78.59,-8.59 79.18,-9.41 79.67,-10.25 80.07,-11.11 80.37,-11.99 80.59,-12.89 80.71,-13.8 80.74,-14.72 80.69,-15.65 80.55,-16.59 80.33,-17.53 80.03,-18.47 79.65,-19.41 79.21,-20.35 78.69,-21.28 78.11,-22.2 77.47,-23.11 76.77,-24.01 76.02,-24.89 75.22,-25.75 74.37,-26.59 73.48,-27.41 72.56,-28.2 71.6,-28.96 70.61,-29.69 69.59,-30.39 68.54,-31.06 67.48,-31.69 66.39,-32.29 65.29,-32.84 64.18,-33.35 63.05,-33.82 61.91,-34.25 60.76,-34.64 59.61,-34.97 58.45,-35.26 57.28,-35.51 56.11,-35.7 54.94,-35.85 53.76,-35.95 52.59,-36 51.41,-36 50.24,-35.95 49.06,-35.85 47.89,-35.7 46.72,-35.51 45.55,-35.26 44.39,-34.97 43.24,-34.64 42.09,-34.25 40.95,-33.82 39.82,-33.35 38.71,-32.84 37.61,-32.29 36.52,-31.69 35.46,-31.06 34.41,-30.39 33.39,-29.69 32.4,-28.96 31.44,-28.2 30.52,-27.41 29.63,-26.59 28.78,-25.75 27.98,-24.89 27.23,-24.01 26.53,-23.11 25.89,-22.2 25.31,-21.28 24.79,-20.35 24.35,-19.41 23.97,-18.47 23.67,-17.53 23.45,-16.59 23.31,-15.65 23.26,-14.72 23.29,-13.8 23.41,-12.89 23.63,-11.99 23.93,-11.11 24.33,-10.25 24.82,-9.41 25.41,-8.59 26.09,-7.8 26.87,-7.04 27.74,-6.31 28.69,-5.61 29.74,-4.94 30.86,-4.31 32.07,-3.71 33.36,-3.16 34.72,-2.65 36.15,-2.18 37.64,-1.75 39.19,-1.36 40.79,-1.03 42.43,-0.74 44.12,-0.49 45.84,-0.3 47.58,-0.15 49.34,-0.05 51.11,0 52.89,0 54.66,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"52\" y=\"-12.95\" 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",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"70.66,-88.55 72.42,-88.65 74.16,-88.8 75.88,-88.99 77.57,-89.24 79.21,-89.53 80.81,-89.86 82.36,-90.25 83.85,-90.68 85.28,-91.15 86.64,-91.66 87.93,-92.21 89.14,-92.81 90.26,-93.44 91.31,-94.11 92.26,-94.81 93.13,-95.54 93.91,-96.3 94.59,-97.09 95.18,-97.91 95.67,-98.75 96.07,-99.61 96.37,-100.49 96.59,-101.39 96.71,-102.3 96.74,-103.22 96.69,-104.15 96.55,-105.09 96.33,-106.03 96.03,-106.97 95.65,-107.91 95.21,-108.85 94.69,-109.78 94.11,-110.7 93.47,-111.61 92.77,-112.51 92.02,-113.39 91.22,-114.25 90.37,-115.09 89.48,-115.91 88.56,-116.7 87.6,-117.46 86.61,-118.19 85.59,-118.89 84.54,-119.56 83.48,-120.19 82.39,-120.79 81.29,-121.34 80.18,-121.85 79.05,-122.32 77.91,-122.75 76.76,-123.14 75.61,-123.47 74.45,-123.76 73.28,-124.01 72.11,-124.2 70.94,-124.35 69.76,-124.45 68.59,-124.5 67.41,-124.5 66.24,-124.45 65.06,-124.35 63.89,-124.2 62.72,-124.01 61.55,-123.76 60.39,-123.47 59.24,-123.14 58.09,-122.75 56.95,-122.32 55.82,-121.85 54.71,-121.34 53.61,-120.79 52.52,-120.19 51.46,-119.56 50.41,-118.89 49.39,-118.19 48.4,-117.46 47.44,-116.7 46.52,-115.91 45.63,-115.09 44.78,-114.25 43.98,-113.39 43.23,-112.51 42.53,-111.61 41.89,-110.7 41.31,-109.78 40.79,-108.85 40.35,-107.91 39.97,-106.97 39.67,-106.03 39.45,-105.09 39.31,-104.15 39.26,-103.22 39.29,-102.3 39.41,-101.39 39.63,-100.49 39.93,-99.61 40.33,-98.75 40.82,-97.91 41.41,-97.09 42.09,-96.3 42.87,-95.54 43.74,-94.81 44.69,-94.11 45.74,-93.44 46.86,-92.81 48.07,-92.21 49.36,-91.66 50.72,-91.15 52.15,-90.68 53.64,-90.25 55.19,-89.86 56.79,-89.53 58.43,-89.24 60.12,-88.99 61.84,-88.8 63.58,-88.65 65.34,-88.55 67.11,-88.5 68.89,-88.5 70.66,-88.55\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-101.45\" 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",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"169,-124.5 115,-124.5 115,-88.5 169,-88.5 169,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"142\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n",
"</g>\n",
"<!-- not(p)->p -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>not(p)->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M124.22,-88.41C109.87,-74.62 89.6,-55.14 74.19,-40.33\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"76.92,-38.1 67.29,-33.69 72.07,-43.15 76.92,-38.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"108.38\" y=\"-57.2\" 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",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"54,-301.5 0,-301.5 0,-265.5 54,-265.5 54,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">and</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->p -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M25.6,-265.22C23.2,-231.15 19.52,-153 30,-88.5 32.31,-74.25 36.94,-58.9 41.35,-46.26\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"44.61,-47.54 44.75,-36.94 38.03,-45.13 44.61,-47.54\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.38\" y=\"-145.7\" 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",
+ "<polygon fill=\"none\" stroke=\"black\" points=\"95,-213 41,-213 41,-177 95,-177 95,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">or</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->or(q,not(p)) -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M35.1,-265.41C40.74,-253.52 48.37,-237.41 54.87,-223.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"58.01,-225.25 59.13,-214.72 51.68,-222.26 58.01,-225.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"54.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- or(q,not(p))->q -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M68,-176.91C68,-165.26 68,-149.55 68,-136.02\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"71.5,-136.36 68,-126.36 64.5,-136.36 71.5,-136.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"71.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(q,not(p))->not(p) -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M82.62,-176.91C93.19,-164.55 107.67,-147.63 119.68,-133.58\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"122.33,-135.87 126.17,-126 117.01,-131.32 122.33,-135.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"114.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -478,14 +654,19 @@
"## 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`.\n",
+ "For example, `and` maps inputs `true` and `false` to `false`. The truth table for the negation is:\n",
+ "\n",
+ "| a | not(a) |\n",
+ "| --- | --- |\n",
+ "| true | false |\n",
+ "| false | true |\n",
"\n",
"Below we encode the truth table for five connectives as Prolog facts and rules."
]
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 15,
"id": "350b9756",
"metadata": {
"vscode": {
@@ -509,6 +690,7 @@
"truth_value(true).\n",
"truth_value(false).\n",
"\n",
+ "% generate a single truth table for all connectives above:\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",
@@ -525,7 +707,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 16,
"id": "3101448b",
"metadata": {
"vscode": {
@@ -544,12 +726,12 @@
}
],
"source": [
- "?- and(true,false,X)."
+ "?- and(true,X,false)."
]
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 17,
"id": "79d16b97",
"metadata": {
"vscode": {
@@ -574,7 +756,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 18,
"id": "d989abf2",
"metadata": {
"vscode": {
@@ -598,7 +780,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 19,
"id": "922004e9",
"metadata": {
"vscode": {
@@ -630,7 +812,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 20,
"id": "54b57ff8",
"metadata": {
"vscode": {
@@ -641,7 +823,7 @@
{
"data": {
"text/markdown": [
- "A | B | NotA | AandB | AorB | AimpliesB | AequivB | \n",
+ "A | B | Not_A | A_and_B | A_or_B | A_implies_B | A_equiv_B | \n",
":- | :- | :- | :- | :- | :- | :- | \n",
"true | true | false | true | true | true | true | \n",
"true | false | false | false | true | false | false | \n",
@@ -649,7 +831,7 @@
"false | false | true | false | false | true | true | "
],
"text/plain": [
- "A | B | NotA | AandB | AorB | AimpliesB | AequivB | \n",
+ "A | B | Not_A | A_and_B | A_or_B | A_implies_B | A_equiv_B | \n",
":- | :- | :- | :- | :- | :- | :- | \n",
"true | true | false | true | true | true | true | \n",
"true | false | false | false | true | false | false | \n",
@@ -671,7 +853,7 @@
}
],
"source": [
- "jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))"
+ "jupyter:print_table(truth_table(A,B,Not_A,A_and_B,A_or_B,A_implies_B,A_equiv_B))"
]
},
{
@@ -679,6 +861,7 @@
"id": "ce32b1d0",
"metadata": {},
"source": [
+ "### Interpretations ###\n",
"An <b>interpretation</b> is an assignment of all relevant proposition to truth values (true or false).\n",
"For example, given the formula `(p∧(q∨(¬p)))` an interpretation needs to assign a truth value to `p` and `q`.\n",
"In the Prolog code below we will represent an interpretation as a list of bindings, each binding is a term of the form `Proposition/TruthValue`.\n",
@@ -689,7 +872,55 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 21,
+ "id": "9a319a34",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mX = 222"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- member(eq(z,X),[eq(p,1),eq(q,2),eq(z,222)])."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "id": "e425b0a3",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mX = 222"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- member(/(z,X),[/(p,1),/(q,2),/(z,222)])."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
"id": "8f6d804b",
"metadata": {
"vscode": {
@@ -714,7 +945,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 24,
"id": "da495155",
"metadata": {
"vscode": {
@@ -749,7 +980,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 25,
"id": "175c00d0",
"metadata": {
"vscode": {
@@ -783,7 +1014,31 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 26,
+ "id": "ecd6951a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = false"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- value(not(p), [p/true, q/false],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
"id": "eee17774",
"metadata": {
"vscode": {
@@ -815,7 +1070,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 28,
"id": "575fc20f",
"metadata": {
"vscode": {
@@ -843,14 +1098,39 @@
"id": "4387b4a2",
"metadata": {},
"source": [
+ "### Models ###\n",
"The truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/true]` is true.\n",
"In this case the interpretation is called a <b>model</b> of the formula."
]
},
{
"cell_type": "code",
- "execution_count": 23,
- "id": "fec75f65",
+ "execution_count": 29,
+ "id": "fec75f65",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = true"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- value(and(p,or(q,not(p))), [p/true, q/true],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "id": "d88c023e",
"metadata": {
"vscode": {
"languageId": "prolog"
@@ -860,7 +1140,8 @@
{
"data": {
"text/plain": [
- "\u001b[1mRes = true"
+ "\u001b[1mP = true,\n",
+ "Q = true"
]
},
"metadata": {},
@@ -868,7 +1149,7 @@
}
],
"source": [
- "?- value(and(p,or(q,not(p))), [p/true, q/true],Res)."
+ "?- value(and(p,or(q,not(p))), [p/P, q/Q],true)."
]
},
{
@@ -882,7 +1163,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 31,
"id": "78473da0",
"metadata": {
"vscode": {
@@ -937,7 +1218,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 32,
"id": "2ee60c15",
"metadata": {
"vscode": {
@@ -962,7 +1243,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 33,
"id": "2b497dad",
"metadata": {
"vscode": {
@@ -976,77 +1257,77 @@
"<?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",
+ "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\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",
+ "<svg width=\"177pt\" height=\"310pt\"\n",
+ " viewBox=\"0.00 0.00 177.00 309.50\" 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 305.5)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-305.5 173,-305.5 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",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"54.66,-0.05 56.42,-0.15 58.16,-0.3 59.88,-0.49 61.57,-0.74 63.21,-1.03 64.81,-1.36 66.36,-1.75 67.85,-2.18 69.28,-2.65 70.64,-3.16 71.93,-3.71 73.14,-4.31 74.26,-4.94 75.31,-5.61 76.26,-6.31 77.13,-7.04 77.91,-7.8 78.59,-8.59 79.18,-9.41 79.67,-10.25 80.07,-11.11 80.37,-11.99 80.59,-12.89 80.71,-13.8 80.74,-14.72 80.69,-15.65 80.55,-16.59 80.33,-17.53 80.03,-18.47 79.65,-19.41 79.21,-20.35 78.69,-21.28 78.11,-22.2 77.47,-23.11 76.77,-24.01 76.02,-24.89 75.22,-25.75 74.37,-26.59 73.48,-27.41 72.56,-28.2 71.6,-28.96 70.61,-29.69 69.59,-30.39 68.54,-31.06 67.48,-31.69 66.39,-32.29 65.29,-32.84 64.18,-33.35 63.05,-33.82 61.91,-34.25 60.76,-34.64 59.61,-34.97 58.45,-35.26 57.28,-35.51 56.11,-35.7 54.94,-35.85 53.76,-35.95 52.59,-36 51.41,-36 50.24,-35.95 49.06,-35.85 47.89,-35.7 46.72,-35.51 45.55,-35.26 44.39,-34.97 43.24,-34.64 42.09,-34.25 40.95,-33.82 39.82,-33.35 38.71,-32.84 37.61,-32.29 36.52,-31.69 35.46,-31.06 34.41,-30.39 33.39,-29.69 32.4,-28.96 31.44,-28.2 30.52,-27.41 29.63,-26.59 28.78,-25.75 27.98,-24.89 27.23,-24.01 26.53,-23.11 25.89,-22.2 25.31,-21.28 24.79,-20.35 24.35,-19.41 23.97,-18.47 23.67,-17.53 23.45,-16.59 23.31,-15.65 23.26,-14.72 23.29,-13.8 23.41,-12.89 23.63,-11.99 23.93,-11.11 24.33,-10.25 24.82,-9.41 25.41,-8.59 26.09,-7.8 26.87,-7.04 27.74,-6.31 28.69,-5.61 29.74,-4.94 30.86,-4.31 32.07,-3.71 33.36,-3.16 34.72,-2.65 36.15,-2.18 37.64,-1.75 39.19,-1.36 40.79,-1.03 42.43,-0.74 44.12,-0.49 45.84,-0.3 47.58,-0.15 49.34,-0.05 51.11,0 52.89,0 54.66,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"52\" y=\"-12.95\" 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",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"70.66,-88.55 72.42,-88.65 74.16,-88.8 75.88,-88.99 77.57,-89.24 79.21,-89.53 80.81,-89.86 82.36,-90.25 83.85,-90.68 85.28,-91.15 86.64,-91.66 87.93,-92.21 89.14,-92.81 90.26,-93.44 91.31,-94.11 92.26,-94.81 93.13,-95.54 93.91,-96.3 94.59,-97.09 95.18,-97.91 95.67,-98.75 96.07,-99.61 96.37,-100.49 96.59,-101.39 96.71,-102.3 96.74,-103.22 96.69,-104.15 96.55,-105.09 96.33,-106.03 96.03,-106.97 95.65,-107.91 95.21,-108.85 94.69,-109.78 94.11,-110.7 93.47,-111.61 92.77,-112.51 92.02,-113.39 91.22,-114.25 90.37,-115.09 89.48,-115.91 88.56,-116.7 87.6,-117.46 86.61,-118.19 85.59,-118.89 84.54,-119.56 83.48,-120.19 82.39,-120.79 81.29,-121.34 80.18,-121.85 79.05,-122.32 77.91,-122.75 76.76,-123.14 75.61,-123.47 74.45,-123.76 73.28,-124.01 72.11,-124.2 70.94,-124.35 69.76,-124.45 68.59,-124.5 67.41,-124.5 66.24,-124.45 65.06,-124.35 63.89,-124.2 62.72,-124.01 61.55,-123.76 60.39,-123.47 59.24,-123.14 58.09,-122.75 56.95,-122.32 55.82,-121.85 54.71,-121.34 53.61,-120.79 52.52,-120.19 51.46,-119.56 50.41,-118.89 49.39,-118.19 48.4,-117.46 47.44,-116.7 46.52,-115.91 45.63,-115.09 44.78,-114.25 43.98,-113.39 43.23,-112.51 42.53,-111.61 41.89,-110.7 41.31,-109.78 40.79,-108.85 40.35,-107.91 39.97,-106.97 39.67,-106.03 39.45,-105.09 39.31,-104.15 39.26,-103.22 39.29,-102.3 39.41,-101.39 39.63,-100.49 39.93,-99.61 40.33,-98.75 40.82,-97.91 41.41,-97.09 42.09,-96.3 42.87,-95.54 43.74,-94.81 44.69,-94.11 45.74,-93.44 46.86,-92.81 48.07,-92.21 49.36,-91.66 50.72,-91.15 52.15,-90.68 53.64,-90.25 55.19,-89.86 56.79,-89.53 58.43,-89.24 60.12,-88.99 61.84,-88.8 63.58,-88.65 65.34,-88.55 67.11,-88.5 68.89,-88.5 70.66,-88.55\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-101.45\" 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\">¬</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-124.5 115,-124.5 115,-88.5 169,-88.5 169,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"142\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(p)->p -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>not(p)->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M124.22,-88.41C109.87,-74.62 89.6,-55.14 74.19,-40.33\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"76.92,-38.1 67.29,-33.69 72.07,-43.15 76.92,-38.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"108.38\" y=\"-57.2\" 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\">∧</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"54,-301.5 0,-301.5 0,-265.5 54,-265.5 54,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->p -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M25.6,-265.22C23.2,-231.15 19.52,-153 30,-88.5 32.31,-74.25 36.94,-58.9 41.35,-46.26\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"44.61,-47.54 44.75,-36.94 38.03,-45.13 44.61,-47.54\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.38\" y=\"-145.7\" 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\">∨</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"95,-213 41,-213 41,-177 95,-177 95,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-188.45\" font-family=\"Times,serif\" font-size=\"14.00\">∨</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->or(q,not(p)) -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M35.1,-265.41C40.74,-253.52 48.37,-237.41 54.87,-223.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"58.01,-225.25 59.13,-214.72 51.68,-222.26 58.01,-225.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"54.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- or(q,not(p))->q -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M68,-176.91C68,-165.26 68,-149.55 68,-136.02\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"71.5,-136.36 68,-126.36 64.5,-136.36 71.5,-136.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"71.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(q,not(p))->not(p) -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M82.62,-176.91C93.19,-164.55 107.67,-147.63 119.68,-133.58\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"122.33,-135.87 126.17,-126 117.01,-131.32 122.33,-135.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"114.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -1085,7 +1366,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 34,
"id": "0fd23f05",
"metadata": {
"vscode": {
@@ -1099,77 +1380,77 @@
"<?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",
+ "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\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",
+ "<svg width=\"177pt\" height=\"310pt\"\n",
+ " viewBox=\"0.00 0.00 177.00 309.50\" 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 305.5)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-305.5 173,-305.5 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",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"54.66,-0.05 56.42,-0.15 58.16,-0.3 59.88,-0.49 61.57,-0.74 63.21,-1.03 64.81,-1.36 66.36,-1.75 67.85,-2.18 69.28,-2.65 70.64,-3.16 71.93,-3.71 73.14,-4.31 74.26,-4.94 75.31,-5.61 76.26,-6.31 77.13,-7.04 77.91,-7.8 78.59,-8.59 79.18,-9.41 79.67,-10.25 80.07,-11.11 80.37,-11.99 80.59,-12.89 80.71,-13.8 80.74,-14.72 80.69,-15.65 80.55,-16.59 80.33,-17.53 80.03,-18.47 79.65,-19.41 79.21,-20.35 78.69,-21.28 78.11,-22.2 77.47,-23.11 76.77,-24.01 76.02,-24.89 75.22,-25.75 74.37,-26.59 73.48,-27.41 72.56,-28.2 71.6,-28.96 70.61,-29.69 69.59,-30.39 68.54,-31.06 67.48,-31.69 66.39,-32.29 65.29,-32.84 64.18,-33.35 63.05,-33.82 61.91,-34.25 60.76,-34.64 59.61,-34.97 58.45,-35.26 57.28,-35.51 56.11,-35.7 54.94,-35.85 53.76,-35.95 52.59,-36 51.41,-36 50.24,-35.95 49.06,-35.85 47.89,-35.7 46.72,-35.51 45.55,-35.26 44.39,-34.97 43.24,-34.64 42.09,-34.25 40.95,-33.82 39.82,-33.35 38.71,-32.84 37.61,-32.29 36.52,-31.69 35.46,-31.06 34.41,-30.39 33.39,-29.69 32.4,-28.96 31.44,-28.2 30.52,-27.41 29.63,-26.59 28.78,-25.75 27.98,-24.89 27.23,-24.01 26.53,-23.11 25.89,-22.2 25.31,-21.28 24.79,-20.35 24.35,-19.41 23.97,-18.47 23.67,-17.53 23.45,-16.59 23.31,-15.65 23.26,-14.72 23.29,-13.8 23.41,-12.89 23.63,-11.99 23.93,-11.11 24.33,-10.25 24.82,-9.41 25.41,-8.59 26.09,-7.8 26.87,-7.04 27.74,-6.31 28.69,-5.61 29.74,-4.94 30.86,-4.31 32.07,-3.71 33.36,-3.16 34.72,-2.65 36.15,-2.18 37.64,-1.75 39.19,-1.36 40.79,-1.03 42.43,-0.74 44.12,-0.49 45.84,-0.3 47.58,-0.15 49.34,-0.05 51.11,0 52.89,0 54.66,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"52\" y=\"-12.95\" 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=\"olive\" 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",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"70.66,-88.55 72.42,-88.65 74.16,-88.8 75.88,-88.99 77.57,-89.24 79.21,-89.53 80.81,-89.86 82.36,-90.25 83.85,-90.68 85.28,-91.15 86.64,-91.66 87.93,-92.21 89.14,-92.81 90.26,-93.44 91.31,-94.11 92.26,-94.81 93.13,-95.54 93.91,-96.3 94.59,-97.09 95.18,-97.91 95.67,-98.75 96.07,-99.61 96.37,-100.49 96.59,-101.39 96.71,-102.3 96.74,-103.22 96.69,-104.15 96.55,-105.09 96.33,-106.03 96.03,-106.97 95.65,-107.91 95.21,-108.85 94.69,-109.78 94.11,-110.7 93.47,-111.61 92.77,-112.51 92.02,-113.39 91.22,-114.25 90.37,-115.09 89.48,-115.91 88.56,-116.7 87.6,-117.46 86.61,-118.19 85.59,-118.89 84.54,-119.56 83.48,-120.19 82.39,-120.79 81.29,-121.34 80.18,-121.85 79.05,-122.32 77.91,-122.75 76.76,-123.14 75.61,-123.47 74.45,-123.76 73.28,-124.01 72.11,-124.2 70.94,-124.35 69.76,-124.45 68.59,-124.5 67.41,-124.5 66.24,-124.45 65.06,-124.35 63.89,-124.2 62.72,-124.01 61.55,-123.76 60.39,-123.47 59.24,-123.14 58.09,-122.75 56.95,-122.32 55.82,-121.85 54.71,-121.34 53.61,-120.79 52.52,-120.19 51.46,-119.56 50.41,-118.89 49.39,-118.19 48.4,-117.46 47.44,-116.7 46.52,-115.91 45.63,-115.09 44.78,-114.25 43.98,-113.39 43.23,-112.51 42.53,-111.61 41.89,-110.7 41.31,-109.78 40.79,-108.85 40.35,-107.91 39.97,-106.97 39.67,-106.03 39.45,-105.09 39.31,-104.15 39.26,-103.22 39.29,-102.3 39.41,-101.39 39.63,-100.49 39.93,-99.61 40.33,-98.75 40.82,-97.91 41.41,-97.09 42.09,-96.3 42.87,-95.54 43.74,-94.81 44.69,-94.11 45.74,-93.44 46.86,-92.81 48.07,-92.21 49.36,-91.66 50.72,-91.15 52.15,-90.68 53.64,-90.25 55.19,-89.86 56.79,-89.53 58.43,-89.24 60.12,-88.99 61.84,-88.8 63.58,-88.65 65.34,-88.55 67.11,-88.5 68.89,-88.5 70.66,-88.55\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-101.45\" 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\">¬</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-124.5 115,-124.5 115,-88.5 169,-88.5 169,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"142\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(p)->p -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>not(p)->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M124.22,-88.41C109.87,-74.62 89.6,-55.14 74.19,-40.33\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"76.92,-38.1 67.29,-33.69 72.07,-43.15 76.92,-38.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"108.38\" y=\"-57.2\" 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=\"olive\" 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\">∧</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"54,-301.5 0,-301.5 0,-265.5 54,-265.5 54,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->p -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M25.6,-265.22C23.2,-231.15 19.52,-153 30,-88.5 32.31,-74.25 36.94,-58.9 41.35,-46.26\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"44.61,-47.54 44.75,-36.94 38.03,-45.13 44.61,-47.54\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.38\" y=\"-145.7\" 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=\"olive\" 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\">∨</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"95,-213 41,-213 41,-177 95,-177 95,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-188.45\" font-family=\"Times,serif\" font-size=\"14.00\">∨</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->or(q,not(p)) -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M35.1,-265.41C40.74,-253.52 48.37,-237.41 54.87,-223.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"58.01,-225.25 59.13,-214.72 51.68,-222.26 58.01,-225.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"54.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- or(q,not(p))->q -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M68,-176.91C68,-165.26 68,-149.55 68,-136.02\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"71.5,-136.36 68,-126.36 64.5,-136.36 71.5,-136.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"71.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(q,not(p))->not(p) -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M82.62,-176.91C93.19,-164.55 107.67,-147.63 119.68,-133.58\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"122.33,-135.87 126.17,-126 117.01,-131.32 122.33,-135.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"114.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -1211,12 +1492,13 @@
"id": "013fda69",
"metadata": {},
"source": [
+ "### Kinds of Formulas ###\n",
"A formula for which all interpretations are models is called a <b>tautology</b>:"
]
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 35,
"id": "23775624",
"metadata": {
"vscode": {
@@ -1258,7 +1540,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 36,
"id": "7a6e29ed",
"metadata": {
"vscode": {
@@ -1312,7 +1594,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 37,
"id": "6bd292f4",
"metadata": {
"vscode": {
@@ -1369,7 +1651,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 38,
"id": "ab15628a",
"metadata": {
"vscode": {
@@ -1407,7 +1689,7 @@
"id": "8b2acc10",
"metadata": {},
"source": [
- "\n",
+ "### Logical Equivalence ###\n",
"Two formulas are called <b>equivalent</b> iff they have the same models.\n",
"We write this as `A ≡ B`.\n",
"\n",
@@ -1417,7 +1699,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 39,
"id": "68a2a19c",
"metadata": {
"vscode": {
@@ -1463,7 +1745,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 40,
"id": "41f43345",
"metadata": {
"vscode": {
@@ -1512,6 +1794,7 @@
"id": "248d3d32",
"metadata": {},
"source": [
+ "### Logical Consequence ###\n",
"A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`.\n",
"We write this as `A ⊨ B`.\n",
"\n",
@@ -1521,7 +1804,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 41,
"id": "aaf46953",
"metadata": {
"vscode": {
@@ -1578,7 +1861,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 42,
"id": "da0a82b5",
"metadata": {
"vscode": {
@@ -1589,7 +1872,7 @@
"source": [
"get_aps(Formula,SortedPropositions) :- \n",
" findall(P, ap(Formula,P), Ps), sort(Ps,SortedPropositions).\n",
- "% extract atomic propostions used by formula\n",
+ "% extract atomic propostions used by formula as a list\n",
"ap(X,X) :- atomic(X).\n",
"ap(and(A,B),AP) :- ap(A,AP) ; ap(B,AP).\n",
"ap(or(A,B),AP) :- ap(A,AP) ; ap(B,AP).\n",
@@ -1600,7 +1883,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 43,
"id": "a216799f",
"metadata": {
"vscode": {
@@ -1624,7 +1907,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 44,
"id": "8a38f7cc",
"metadata": {
"vscode": {
@@ -1648,7 +1931,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 45,
"id": "82980216",
"metadata": {
"vscode": {
@@ -1680,7 +1963,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 46,
"id": "23cfb806",
"metadata": {
"vscode": {
@@ -1710,7 +1993,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 47,
"id": "da991b8d",
"metadata": {
"vscode": {
@@ -1721,7 +2004,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mR = [a/_55832,b/_55844,c/_55856]"
+ "\u001b[1mR = [a/_20916,b/_20928,c/_20940]"
]
},
"metadata": {},
@@ -1742,7 +2025,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": 48,
"id": "6338f6bf",
"metadata": {
"vscode": {
@@ -1766,7 +2049,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 49,
"id": "266a4bd8",
"metadata": {
"vscode": {
@@ -1802,7 +2085,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": 50,
"id": "6957d9f3",
"metadata": {
"vscode": {
@@ -1817,9 +2100,17 @@
"equivalent(A,B) :- prove(A,B), prove(B,A)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "0164a7ec",
+ "metadata": {},
+ "source": [
+ "For example, we can now prove that ```p or q``` is a logical consequence of ```p and q```:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 44,
+ "execution_count": 51,
"id": "f552a71e",
"metadata": {
"vscode": {
@@ -1841,9 +2132,21 @@
"?- prove(and(p,q),or(p,q))."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "0f4331e3",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "However, the logical consequence does not hold the other way around:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 52,
"id": "76b8ab5a",
"metadata": {
"vscode": {
@@ -1867,7 +2170,7 @@
},
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 53,
"id": "f8aca8b7",
"metadata": {
"vscode": {
@@ -1889,9 +2192,17 @@
"?- equivalent(and(p,q),or(p,q))."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "e60f533e",
+ "metadata": {},
+ "source": [
+ "As usual in classical logic, anything is a consequence of a contradiction:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 49,
+ "execution_count": 54,
"id": "e7a2828d",
"metadata": {
"vscode": {
@@ -1909,6 +2220,30 @@
"output_type": "display_data"
}
],
+ "source": [
+ "?- prove(and(p,not(p)),q)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 55,
+ "id": "47dd7088",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
"source": [
"?- prove(and(p,not(p)),and(q,not(q)))."
]
@@ -1923,7 +2258,7 @@
},
{
"cell_type": "code",
- "execution_count": 50,
+ "execution_count": 56,
"id": "26bab55b",
"metadata": {
"vscode": {
@@ -1938,7 +2273,7 @@
},
{
"cell_type": "code",
- "execution_count": 51,
+ "execution_count": 57,
"id": "fe5daeb4",
"metadata": {
"vscode": {
@@ -1977,7 +2312,7 @@
},
{
"cell_type": "code",
- "execution_count": 52,
+ "execution_count": 58,
"id": "3187bee7",
"metadata": {
"vscode": {
@@ -1999,17 +2334,49 @@
"?- sat(and(equiv(a,or(not(b),not(c))),equiv(b,a)),I)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "31253833",
+ "metadata": {},
+ "source": [
+ "And we can find no further solution to this query:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 59,
+ "id": "b79ef066",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:retry."
+ ]
+ },
{
"cell_type": "markdown",
"id": "575d68a0",
"metadata": {},
"source": [
- "We can also prove that this is the only solution, i.e., our puzzle implies that A and B are knights and C is a knave:"
+ "We can also prove explicitly that this is the only solution, i.e., our puzzle implies that A and B are knights and C is a knave:"
]
},
{
"cell_type": "code",
- "execution_count": 53,
+ "execution_count": 60,
"id": "df153b0a",
"metadata": {
"vscode": {
@@ -2033,7 +2400,7 @@
},
{
"cell_type": "code",
- "execution_count": 54,
+ "execution_count": 61,
"id": "1712e9e0",
"metadata": {
"vscode": {
@@ -2047,136 +2414,136 @@
"<?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",
+ "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
- "<svg width=\"176pt\" height=\"392pt\"\n",
- " viewBox=\"0.00 0.00 176.49 392.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 388)\">\n",
- "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-388 172.49,-388 172.49,4 -4,4\"/>\n",
+ "<svg width=\"176pt\" height=\"398pt\"\n",
+ " viewBox=\"0.00 0.00 176.49 398.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 394)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-394 172.49,-394 172.49,4 -4,4\"/>\n",
"<!-- a -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>a</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"105.43,-174.05 107.2,-174.15 108.96,-174.3 110.69,-174.49 112.39,-174.74 114.05,-175.03 115.67,-175.36 117.23,-175.75 118.73,-176.18 120.17,-176.65 121.54,-177.16 122.84,-177.71 124.06,-178.31 125.2,-178.94 126.25,-179.61 127.22,-180.31 128.09,-181.04 128.87,-181.8 129.56,-182.59 130.15,-183.41 130.65,-184.25 131.05,-185.11 131.36,-185.99 131.58,-186.89 131.7,-187.8 131.73,-188.72 131.68,-189.65 131.54,-190.59 131.31,-191.53 131.01,-192.47 130.63,-193.41 130.18,-194.35 129.66,-195.28 129.08,-196.2 128.43,-197.11 127.72,-198.01 126.97,-198.89 126.16,-199.75 125.3,-200.59 124.41,-201.41 123.48,-202.2 122.51,-202.96 121.51,-203.69 120.48,-204.39 119.43,-205.06 118.35,-205.69 117.26,-206.29 116.15,-206.84 115.02,-207.35 113.89,-207.82 112.74,-208.25 111.58,-208.64 110.42,-208.97 109.24,-209.26 108.07,-209.51 106.89,-209.7 105.71,-209.85 104.52,-209.95 103.34,-210 102.15,-210 100.96,-209.95 99.78,-209.85 98.6,-209.7 97.42,-209.51 96.24,-209.26 95.07,-208.97 93.91,-208.64 92.75,-208.25 91.6,-207.82 90.46,-207.35 89.34,-206.84 88.23,-206.29 87.13,-205.69 86.06,-205.06 85.01,-204.39 83.98,-203.69 82.98,-202.96 82.01,-202.2 81.08,-201.41 80.18,-200.59 79.33,-199.75 78.52,-198.89 77.76,-198.01 77.06,-197.11 76.41,-196.2 75.83,-195.28 75.3,-194.35 74.85,-193.41 74.47,-192.47 74.17,-191.53 73.95,-190.59 73.81,-189.65 73.75,-188.72 73.79,-187.8 73.91,-186.89 74.13,-185.99 74.43,-185.11 74.84,-184.25 75.34,-183.41 75.93,-182.59 76.62,-181.8 77.4,-181.04 78.27,-180.31 79.24,-179.61 80.29,-178.94 81.43,-178.31 82.65,-177.71 83.94,-177.16 85.31,-176.65 86.75,-176.18 88.26,-175.75 89.82,-175.36 91.44,-175.03 93.1,-174.74 94.79,-174.49 96.53,-174.3 98.28,-174.15 100.06,-174.05 101.85,-174 103.64,-174 105.43,-174.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"102.74\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"105.4,-177.05 107.16,-177.15 108.91,-177.3 110.62,-177.49 112.31,-177.74 113.96,-178.03 115.56,-178.36 117.11,-178.75 118.6,-179.18 120.02,-179.65 121.38,-180.16 122.67,-180.71 123.88,-181.31 125.01,-181.94 126.05,-182.61 127.01,-183.31 127.87,-184.04 128.65,-184.8 129.33,-185.59 129.92,-186.41 130.41,-187.25 130.81,-188.11 131.12,-188.99 131.33,-189.89 131.45,-190.8 131.49,-191.72 131.43,-192.65 131.29,-193.59 131.07,-194.53 130.77,-195.47 130.4,-196.41 129.95,-197.35 129.43,-198.28 128.85,-199.2 128.21,-200.11 127.51,-201.01 126.76,-201.89 125.96,-202.75 125.11,-203.59 124.23,-204.41 123.3,-205.2 122.34,-205.96 121.35,-206.69 120.33,-207.39 119.29,-208.06 118.22,-208.69 117.14,-209.29 116.04,-209.84 114.92,-210.35 113.79,-210.82 112.65,-211.25 111.51,-211.64 110.35,-211.97 109.19,-212.26 108.02,-212.51 106.85,-212.7 105.68,-212.85 104.51,-212.95 103.33,-213 102.16,-213 100.98,-212.95 99.81,-212.85 98.63,-212.7 97.46,-212.51 96.3,-212.26 95.14,-211.97 93.98,-211.64 92.83,-211.25 91.7,-210.82 90.57,-210.35 89.45,-209.84 88.35,-209.29 87.27,-208.69 86.2,-208.06 85.16,-207.39 84.14,-206.69 83.15,-205.96 82.19,-205.2 81.26,-204.41 80.37,-203.59 79.53,-202.75 78.73,-201.89 77.97,-201.01 77.28,-200.11 76.63,-199.2 76.05,-198.28 75.54,-197.35 75.09,-196.41 74.71,-195.47 74.41,-194.53 74.19,-193.59 74.05,-192.65 74,-191.72 74.03,-190.8 74.16,-189.89 74.37,-188.99 74.67,-188.11 75.07,-187.25 75.57,-186.41 76.16,-185.59 76.84,-184.8 77.61,-184.04 78.48,-183.31 79.44,-182.61 80.48,-181.94 81.61,-181.31 82.82,-180.71 84.1,-180.16 85.46,-179.65 86.89,-179.18 88.38,-178.75 89.93,-178.36 91.53,-178.03 93.18,-177.74 94.86,-177.49 96.58,-177.3 98.32,-177.15 100.08,-177.05 101.86,-177 103.63,-177 105.4,-177.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102.74\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- b -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>b</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"142.43,-0.05 144.2,-0.15 145.96,-0.3 147.69,-0.49 149.39,-0.74 151.05,-1.03 152.67,-1.36 154.23,-1.75 155.73,-2.18 157.17,-2.65 158.54,-3.16 159.84,-3.71 161.06,-4.31 162.2,-4.94 163.25,-5.61 164.22,-6.31 165.09,-7.04 165.87,-7.8 166.56,-8.59 167.15,-9.41 167.65,-10.25 168.05,-11.11 168.36,-11.99 168.58,-12.89 168.7,-13.8 168.73,-14.72 168.68,-15.65 168.54,-16.59 168.31,-17.53 168.01,-18.47 167.63,-19.41 167.18,-20.35 166.66,-21.28 166.08,-22.2 165.43,-23.11 164.72,-24.01 163.97,-24.89 163.16,-25.75 162.3,-26.59 161.41,-27.41 160.48,-28.2 159.51,-28.96 158.51,-29.69 157.48,-30.39 156.43,-31.06 155.35,-31.69 154.26,-32.29 153.15,-32.84 152.02,-33.35 150.89,-33.82 149.74,-34.25 148.58,-34.64 147.42,-34.97 146.24,-35.26 145.07,-35.51 143.89,-35.7 142.71,-35.85 141.52,-35.95 140.34,-36 139.15,-36 137.96,-35.95 136.78,-35.85 135.6,-35.7 134.42,-35.51 133.24,-35.26 132.07,-34.97 130.91,-34.64 129.75,-34.25 128.6,-33.82 127.46,-33.35 126.34,-32.84 125.23,-32.29 124.13,-31.69 123.06,-31.06 122.01,-30.39 120.98,-29.69 119.98,-28.96 119.01,-28.2 118.08,-27.41 117.18,-26.59 116.33,-25.75 115.52,-24.89 114.76,-24.01 114.06,-23.11 113.41,-22.2 112.83,-21.28 112.3,-20.35 111.85,-19.41 111.47,-18.47 111.17,-17.53 110.95,-16.59 110.81,-15.65 110.75,-14.72 110.79,-13.8 110.91,-12.89 111.13,-11.99 111.43,-11.11 111.84,-10.25 112.34,-9.41 112.93,-8.59 113.62,-7.8 114.4,-7.04 115.27,-6.31 116.24,-5.61 117.29,-4.94 118.43,-4.31 119.65,-3.71 120.94,-3.16 122.31,-2.65 123.75,-2.18 125.26,-1.75 126.82,-1.36 128.44,-1.03 130.1,-0.74 131.79,-0.49 133.53,-0.3 135.28,-0.15 137.06,-0.05 138.85,0 140.64,0 142.43,-0.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"139.74\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"142.4,-0.05 144.16,-0.15 145.91,-0.3 147.62,-0.49 149.31,-0.74 150.96,-1.03 152.56,-1.36 154.11,-1.75 155.6,-2.18 157.02,-2.65 158.38,-3.16 159.67,-3.71 160.88,-4.31 162.01,-4.94 163.05,-5.61 164.01,-6.31 164.87,-7.04 165.65,-7.8 166.33,-8.59 166.92,-9.41 167.41,-10.25 167.81,-11.11 168.12,-11.99 168.33,-12.89 168.45,-13.8 168.49,-14.72 168.43,-15.65 168.29,-16.59 168.07,-17.53 167.77,-18.47 167.4,-19.41 166.95,-20.35 166.43,-21.28 165.85,-22.2 165.21,-23.11 164.51,-24.01 163.76,-24.89 162.96,-25.75 162.11,-26.59 161.23,-27.41 160.3,-28.2 159.34,-28.96 158.35,-29.69 157.33,-30.39 156.29,-31.06 155.22,-31.69 154.14,-32.29 153.04,-32.84 151.92,-33.35 150.79,-33.82 149.65,-34.25 148.51,-34.64 147.35,-34.97 146.19,-35.26 145.02,-35.51 143.85,-35.7 142.68,-35.85 141.51,-35.95 140.33,-36 139.16,-36 137.98,-35.95 136.81,-35.85 135.63,-35.7 134.46,-35.51 133.3,-35.26 132.14,-34.97 130.98,-34.64 129.83,-34.25 128.7,-33.82 127.57,-33.35 126.45,-32.84 125.35,-32.29 124.27,-31.69 123.2,-31.06 122.16,-30.39 121.14,-29.69 120.15,-28.96 119.19,-28.2 118.26,-27.41 117.37,-26.59 116.53,-25.75 115.73,-24.89 114.97,-24.01 114.28,-23.11 113.63,-22.2 113.05,-21.28 112.54,-20.35 112.09,-19.41 111.71,-18.47 111.41,-17.53 111.19,-16.59 111.05,-15.65 111,-14.72 111.03,-13.8 111.16,-12.89 111.37,-11.99 111.67,-11.11 112.07,-10.25 112.57,-9.41 113.16,-8.59 113.84,-7.8 114.61,-7.04 115.48,-6.31 116.44,-5.61 117.48,-4.94 118.61,-4.31 119.82,-3.71 121.1,-3.16 122.46,-2.65 123.89,-2.18 125.38,-1.75 126.93,-1.36 128.53,-1.03 130.18,-0.74 131.86,-0.49 133.58,-0.3 135.32,-0.15 137.08,-0.05 138.86,0 140.63,0 142.4,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.74\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- c -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>c</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"31.43,-0.05 33.2,-0.15 34.96,-0.3 36.69,-0.49 38.39,-0.74 40.05,-1.03 41.67,-1.36 43.23,-1.75 44.73,-2.18 46.17,-2.65 47.54,-3.16 48.84,-3.71 50.06,-4.31 51.2,-4.94 52.25,-5.61 53.22,-6.31 54.09,-7.04 54.87,-7.8 55.56,-8.59 56.15,-9.41 56.65,-10.25 57.05,-11.11 57.36,-11.99 57.58,-12.89 57.7,-13.8 57.73,-14.72 57.68,-15.65 57.54,-16.59 57.31,-17.53 57.01,-18.47 56.63,-19.41 56.18,-20.35 55.66,-21.28 55.08,-22.2 54.43,-23.11 53.72,-24.01 52.97,-24.89 52.16,-25.75 51.3,-26.59 50.41,-27.41 49.48,-28.2 48.51,-28.96 47.51,-29.69 46.48,-30.39 45.43,-31.06 44.35,-31.69 43.26,-32.29 42.15,-32.84 41.02,-33.35 39.89,-33.82 38.74,-34.25 37.58,-34.64 36.42,-34.97 35.24,-35.26 34.07,-35.51 32.89,-35.7 31.71,-35.85 30.52,-35.95 29.34,-36 28.15,-36 26.96,-35.95 25.78,-35.85 24.6,-35.7 23.42,-35.51 22.24,-35.26 21.07,-34.97 19.91,-34.64 18.75,-34.25 17.6,-33.82 16.46,-33.35 15.34,-32.84 14.23,-32.29 13.13,-31.69 12.06,-31.06 11.01,-30.39 9.98,-29.69 8.98,-28.96 8.01,-28.2 7.08,-27.41 6.18,-26.59 5.33,-25.75 4.52,-24.89 3.76,-24.01 3.06,-23.11 2.41,-22.2 1.83,-21.28 1.3,-20.35 0.85,-19.41 0.47,-18.47 0.17,-17.53 -0.05,-16.59 -0.19,-15.65 -0.25,-14.72 -0.21,-13.8 -0.09,-12.89 0.13,-11.99 0.43,-11.11 0.84,-10.25 1.34,-9.41 1.93,-8.59 2.62,-7.8 3.4,-7.04 4.27,-6.31 5.24,-5.61 6.29,-4.94 7.43,-4.31 8.65,-3.71 9.94,-3.16 11.31,-2.65 12.75,-2.18 14.26,-1.75 15.82,-1.36 17.44,-1.03 19.1,-0.74 20.79,-0.49 22.53,-0.3 24.28,-0.15 26.06,-0.05 27.85,0 29.64,0 31.43,-0.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"28.74\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"31.4,-0.05 33.16,-0.15 34.91,-0.3 36.62,-0.49 38.31,-0.74 39.96,-1.03 41.56,-1.36 43.11,-1.75 44.6,-2.18 46.02,-2.65 47.38,-3.16 48.67,-3.71 49.88,-4.31 51.01,-4.94 52.05,-5.61 53.01,-6.31 53.87,-7.04 54.65,-7.8 55.33,-8.59 55.92,-9.41 56.41,-10.25 56.81,-11.11 57.12,-11.99 57.33,-12.89 57.45,-13.8 57.49,-14.72 57.43,-15.65 57.29,-16.59 57.07,-17.53 56.77,-18.47 56.4,-19.41 55.95,-20.35 55.43,-21.28 54.85,-22.2 54.21,-23.11 53.51,-24.01 52.76,-24.89 51.96,-25.75 51.11,-26.59 50.23,-27.41 49.3,-28.2 48.34,-28.96 47.35,-29.69 46.33,-30.39 45.29,-31.06 44.22,-31.69 43.14,-32.29 42.04,-32.84 40.92,-33.35 39.79,-33.82 38.65,-34.25 37.51,-34.64 36.35,-34.97 35.19,-35.26 34.02,-35.51 32.85,-35.7 31.68,-35.85 30.51,-35.95 29.33,-36 28.16,-36 26.98,-35.95 25.81,-35.85 24.63,-35.7 23.46,-35.51 22.3,-35.26 21.14,-34.97 19.98,-34.64 18.83,-34.25 17.7,-33.82 16.57,-33.35 15.45,-32.84 14.35,-32.29 13.27,-31.69 12.2,-31.06 11.16,-30.39 10.14,-29.69 9.15,-28.96 8.19,-28.2 7.26,-27.41 6.37,-26.59 5.53,-25.75 4.73,-24.89 3.97,-24.01 3.28,-23.11 2.63,-22.2 2.05,-21.28 1.54,-20.35 1.09,-19.41 0.71,-18.47 0.41,-17.53 0.19,-16.59 0.05,-15.65 0,-14.72 0.03,-13.8 0.16,-12.89 0.37,-11.99 0.67,-11.11 1.07,-10.25 1.57,-9.41 2.16,-8.59 2.84,-7.8 3.61,-7.04 4.48,-6.31 5.44,-5.61 6.48,-4.94 7.61,-4.31 8.82,-3.71 10.1,-3.16 11.46,-2.65 12.89,-2.18 14.38,-1.75 15.93,-1.36 17.53,-1.03 19.18,-0.74 20.86,-0.49 22.58,-0.3 24.32,-0.15 26.08,-0.05 27.86,0 29.63,0 31.4,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.74\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
"</g>\n",
"<!-- not(b) -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>not(b)</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"129.74,-123 75.74,-123 75.74,-87 129.74,-87 129.74,-123\"/>\n",
- "<text text-anchor=\"middle\" x=\"102.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"129.74,-124.5 75.74,-124.5 75.74,-88.5 129.74,-88.5 129.74,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102.74\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(b)->b -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>not(b)->b</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M110.23,-86.8C115.5,-74.7 122.64,-58.29 128.58,-44.65\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"131.86,-45.88 132.64,-35.31 125.44,-43.08 131.86,-45.88\"/>\n",
- "<text text-anchor=\"middle\" x=\"126.24\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M110.05,-88.41C115.24,-76.29 122.3,-59.78 128.24,-45.9\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"131.39,-47.43 132.1,-36.86 124.95,-44.68 131.39,-47.43\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.12\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- not(c) -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>not(c)</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"55.74,-123 1.74,-123 1.74,-87 55.74,-87 55.74,-123\"/>\n",
- "<text text-anchor=\"middle\" x=\"28.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"55.74,-124.5 1.74,-124.5 1.74,-88.5 55.74,-88.5 55.74,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.74\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(c)->c -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>not(c)->c</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M28.74,-86.8C28.74,-75.16 28.74,-59.55 28.74,-46.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"32.24,-46.18 28.74,-36.18 25.24,-46.18 32.24,-46.18\"/>\n",
- "<text text-anchor=\"middle\" x=\"32.24\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M28.74,-88.41C28.74,-76.76 28.74,-61.05 28.74,-47.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"32.24,-47.86 28.74,-37.86 25.24,-47.86 32.24,-47.86\"/>\n",
+ "<text text-anchor=\"middle\" x=\"32.12\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- and(equiv(a,or(not(b),not(c))),equiv(b,a)) -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>and(equiv(a,or(not(b),not(c))),equiv(b,a))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"126.74,-384 72.74,-384 72.74,-348 126.74,-348 126.74,-384\"/>\n",
- "<text text-anchor=\"middle\" x=\"99.74\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"126.74,-390 72.74,-390 72.74,-354 126.74,-354 126.74,-390\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99.74\" y=\"-365.45\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- equiv(a,or(not(b),not(c))) -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>equiv(a,or(not(b),not(c)))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"90.74,-297 36.74,-297 36.74,-261 90.74,-261 90.74,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"63.74\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"90.74,-301.5 36.74,-301.5 36.74,-265.5 90.74,-265.5 90.74,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"63.74\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
"</g>\n",
"<!-- and(equiv(a,or(not(b),not(c))),equiv(b,a))->equiv(a,or(not(b),not(c))) -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>and(equiv(a,or(not(b),not(c))),equiv(b,a))->equiv(a,or(not(b),not(c)))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M92.46,-347.8C87.43,-335.93 80.65,-319.93 74.95,-306.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"78.14,-305.02 71.02,-297.18 71.69,-307.75 78.14,-305.02\"/>\n",
- "<text text-anchor=\"middle\" x=\"87.24\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M92.63,-353.91C87.68,-342.02 80.98,-325.91 75.27,-312.2\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"78.62,-311.14 71.55,-303.25 72.16,-313.82 78.62,-311.14\"/>\n",
+ "<text text-anchor=\"middle\" x=\"88.12\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(b,a) -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>equiv(b,a)</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"162.74,-297 108.74,-297 108.74,-261 162.74,-261 162.74,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"135.74\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"162.74,-301.5 108.74,-301.5 108.74,-265.5 162.74,-265.5 162.74,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"135.74\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
"</g>\n",
"<!-- and(equiv(a,or(not(b),not(c))),equiv(b,a))->equiv(b,a) -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>and(equiv(a,or(not(b),not(c))),equiv(b,a))->equiv(b,a)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M107.03,-347.8C112.05,-335.93 118.83,-319.93 124.54,-306.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"127.79,-307.75 128.47,-297.18 121.35,-305.02 127.79,-307.75\"/>\n",
- "<text text-anchor=\"middle\" x=\"123.24\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M106.86,-353.91C111.8,-342.02 118.51,-325.91 124.21,-312.2\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"127.33,-313.82 127.94,-303.25 120.87,-311.14 127.33,-313.82\"/>\n",
+ "<text text-anchor=\"middle\" x=\"124.12\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(a,or(not(b),not(c)))->a -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>equiv(a,or(not(b),not(c)))->a</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M71.64,-260.8C77.19,-248.7 84.71,-232.29 90.97,-218.65\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"94.27,-219.86 95.26,-209.31 87.91,-216.94 94.27,-219.86\"/>\n",
- "<text text-anchor=\"middle\" x=\"88.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M71.45,-265.41C76.91,-253.29 84.36,-236.78 90.62,-222.9\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"93.78,-224.4 94.7,-213.85 87.4,-221.52 93.78,-224.4\"/>\n",
+ "<text text-anchor=\"middle\" x=\"89.12\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(not(b),not(c)) -->\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>or(not(b),not(c))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"55.74,-210 1.74,-210 1.74,-174 55.74,-174 55.74,-210\"/>\n",
- "<text text-anchor=\"middle\" x=\"28.74\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">∨</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"55.74,-213 1.74,-213 1.74,-177 55.74,-177 55.74,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.74\" y=\"-188.45\" font-family=\"Times,serif\" font-size=\"14.00\">∨</text>\n",
"</g>\n",
"<!-- equiv(a,or(not(b),not(c)))->or(not(b),not(c)) -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>equiv(a,or(not(b),not(c)))->or(not(b),not(c))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M56.66,-260.8C51.77,-248.93 45.18,-232.93 39.63,-219.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"42.86,-218.09 35.82,-210.18 36.39,-220.75 42.86,-218.09\"/>\n",
- "<text text-anchor=\"middle\" x=\"52.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M56.83,-265.41C52.02,-253.52 45.5,-237.41 39.95,-223.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"43.33,-222.71 36.33,-214.75 36.84,-225.34 43.33,-222.71\"/>\n",
+ "<text text-anchor=\"middle\" x=\"53.12\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(b,a)->a -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>equiv(b,a)->a</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M129.07,-260.8C124.37,-248.7 118,-232.29 112.7,-218.65\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"115.96,-217.37 109.08,-209.31 109.43,-219.9 115.96,-217.37\"/>\n",
- "<text text-anchor=\"middle\" x=\"124.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M129.22,-265.41C124.63,-253.37 118.38,-236.99 113.11,-223.17\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"116.51,-222.27 109.68,-214.17 109.97,-224.76 116.51,-222.27\"/>\n",
+ "<text text-anchor=\"middle\" x=\"125.12\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(b,a)->b -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>equiv(b,a)->b</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M137.34,-260.97C138.55,-247.23 140.1,-227.39 140.74,-210 142.89,-151.64 141.61,-83.18 140.6,-46.14\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"144.1,-46.02 140.31,-36.13 137.1,-46.22 144.1,-46.02\"/>\n",
- "<text text-anchor=\"middle\" x=\"145.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M137.34,-265.1C138.55,-251.05 140.11,-230.77 140.74,-213 142.85,-154.23 141.62,-85.38 140.62,-47.54\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"144.13,-47.81 140.35,-37.91 137.13,-48 144.13,-47.81\"/>\n",
+ "<text text-anchor=\"middle\" x=\"145.12\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(not(b),not(c))->not(b) -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>or(not(b),not(c))->not(b)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M43.72,-173.8C54.45,-161.47 69.07,-144.68 81.07,-130.89\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"83.86,-133.02 87.79,-123.18 78.58,-128.42 83.86,-133.02\"/>\n",
- "<text text-anchor=\"middle\" x=\"73.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M43.36,-176.91C53.94,-164.55 68.41,-147.63 80.43,-133.58\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"83.08,-135.87 86.92,-126 77.76,-131.32 83.08,-135.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"75.12\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(not(b),not(c))->not(c) -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>or(not(b),not(c))->not(c)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M28.74,-173.8C28.74,-162.16 28.74,-146.55 28.74,-133.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"32.24,-133.18 28.74,-123.18 25.24,-133.18 32.24,-133.18\"/>\n",
- "<text text-anchor=\"middle\" x=\"32.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M28.74,-176.91C28.74,-165.26 28.74,-149.55 28.74,-136.02\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"32.24,-136.36 28.74,-126.36 25.24,-136.36 32.24,-136.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"32.12\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -2232,12 +2599,18 @@
"- The King says: One note tells the truth and one does not\n",
"- Note on Door 1: This cell contains a princess and there is a tiger in the other cell\n",
"- Note on Door 2: One of the cells contains a princess and the other one contains a tiger.\n",
- "\n"
+ "\n",
+ "The propositions are\n",
+ "- z1: note on door 1 is true\n",
+ "- z2: note on door 2 is true\n",
+ "- t1: there is a tiger behind door 1 (and no princess behind door 1)\n",
+ "- t2: there is a tiger behind door 2 (and no princess behind dorr 2)\n",
+ "We assume that if t1 is false, then there is a princess behind the door. The same holds for t2."
]
},
{
"cell_type": "code",
- "execution_count": 55,
+ "execution_count": 62,
"id": "4363c114",
"metadata": {
"vscode": {
@@ -2256,12 +2629,14 @@
}
],
"source": [
- "?- sat(and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))),I)."
+ "?- sat(and(equiv(z1,not(z2)),\n",
+ " and(equiv(z1,and(not(t1),t2)),\n",
+ " equiv(z2,equiv(t1,not(t2))))),I)."
]
},
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 63,
"id": "0919b40c",
"metadata": {
"vscode": {
@@ -2283,9 +2658,127 @@
"jupyter:retry."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "38574a7c",
+ "metadata": {},
+ "source": [
+ "Below is an encoding of the puzzle where we do not assume that each cell has either a tiger or a princess; hence we have two atomic propositions per cell (t1,p1 and t2,p2). In this case we do not have a unique solution. So the knowledge that each cell contains one tiger or princess is essential."
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 57,
+ "execution_count": 64,
+ "id": "f2b747ca",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mI = [p1/true,p2/true,t1/true,t2/false,z1/false,z2/true]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- sat(and(equiv(z1,not(z2)),\n",
+ " and(equiv(z1,and(p1,t2)),\n",
+ " equiv(z2,or(and(p1,t2),and(p2,t1))))),I)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 65,
+ "id": "d734608a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mI = [p1/false,p2/true,t1/true,t2/true,z1/false,z2/true]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:retry."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1eaff825",
+ "metadata": {},
+ "source": [
+ "If we add explicitly that t1 is equivalent to not(p1) and ditto for t2 then we have a single solution:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 78,
+ "id": "39802240",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mI = [p1/false,p2/true,t1/true,t2/false,z1/false,z2/true]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- sat(and(equiv(z1,not(z2)),\n",
+ " and(equiv(t1,not(p1)),\n",
+ " and(equiv(t2,not(p2)),\n",
+ " and(equiv(z1,and(p1,t2)),\n",
+ " equiv(z2,or(and(p1,t2),and(p2,t1))))))),I)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 79,
+ "id": "becfaa25",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:retry."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 67,
"id": "f64a00fe",
"metadata": {
"vscode": {
@@ -2299,215 +2792,215 @@
"<?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",
+ "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
- "<svg width=\"286pt\" height=\"479pt\"\n",
- " viewBox=\"0.00 0.00 285.74 479.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 475)\">\n",
- "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-475 281.74,-475 281.74,4 -4,4\"/>\n",
+ "<svg width=\"286pt\" height=\"487pt\"\n",
+ " viewBox=\"0.00 0.00 285.74 486.50\" 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 482.5)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-482.5 281.74,-482.5 281.74,4 -4,4\"/>\n",
"<!-- t1 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>t1</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"152.68,-0.05 154.46,-0.15 156.22,-0.3 157.95,-0.49 159.65,-0.74 161.31,-1.03 162.92,-1.36 164.48,-1.75 165.99,-2.18 167.43,-2.65 168.8,-3.16 170.1,-3.71 171.32,-4.31 172.45,-4.94 173.51,-5.61 174.47,-6.31 175.35,-7.04 176.13,-7.8 176.81,-8.59 177.41,-9.41 177.91,-10.25 178.31,-11.11 178.62,-11.99 178.83,-12.89 178.96,-13.8 178.99,-14.72 178.93,-15.65 178.79,-16.59 178.57,-17.53 178.27,-18.47 177.89,-19.41 177.44,-20.35 176.92,-21.28 176.33,-22.2 175.69,-23.11 174.98,-24.01 174.22,-24.89 173.41,-25.75 172.56,-26.59 171.67,-27.41 170.73,-28.2 169.76,-28.96 168.76,-29.69 167.74,-30.39 166.68,-31.06 165.61,-31.69 164.52,-32.29 163.41,-32.84 162.28,-33.35 161.14,-33.82 159.99,-34.25 158.84,-34.64 157.67,-34.97 156.5,-35.26 155.33,-35.51 154.15,-35.7 152.96,-35.85 151.78,-35.95 150.59,-36 149.41,-36 148.22,-35.95 147.04,-35.85 145.85,-35.7 144.67,-35.51 143.5,-35.26 142.33,-34.97 141.16,-34.64 140.01,-34.25 138.86,-33.82 137.72,-33.35 136.59,-32.84 135.48,-32.29 134.39,-31.69 133.32,-31.06 132.26,-30.39 131.24,-29.69 130.24,-28.96 129.27,-28.2 128.33,-27.41 127.44,-26.59 126.59,-25.75 125.78,-24.89 125.02,-24.01 124.31,-23.11 123.67,-22.2 123.08,-21.28 122.56,-20.35 122.11,-19.41 121.73,-18.47 121.43,-17.53 121.21,-16.59 121.07,-15.65 121.01,-14.72 121.04,-13.8 121.17,-12.89 121.38,-11.99 121.69,-11.11 122.09,-10.25 122.59,-9.41 123.19,-8.59 123.87,-7.8 124.65,-7.04 125.53,-6.31 126.49,-5.61 127.55,-4.94 128.68,-4.31 129.9,-3.71 131.2,-3.16 132.57,-2.65 134.01,-2.18 135.52,-1.75 137.08,-1.36 138.69,-1.03 140.35,-0.74 142.05,-0.49 143.78,-0.3 145.54,-0.15 147.32,-0.05 149.1,0 150.9,0 152.68,-0.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"150\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">t1</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"152.66,-0.05 154.42,-0.15 156.16,-0.3 157.88,-0.49 159.57,-0.74 161.21,-1.03 162.81,-1.36 164.36,-1.75 165.85,-2.18 167.28,-2.65 168.64,-3.16 169.93,-3.71 171.14,-4.31 172.26,-4.94 173.31,-5.61 174.26,-6.31 175.13,-7.04 175.91,-7.8 176.59,-8.59 177.18,-9.41 177.67,-10.25 178.07,-11.11 178.37,-11.99 178.59,-12.89 178.71,-13.8 178.74,-14.72 178.69,-15.65 178.55,-16.59 178.33,-17.53 178.03,-18.47 177.65,-19.41 177.21,-20.35 176.69,-21.28 176.11,-22.2 175.47,-23.11 174.77,-24.01 174.02,-24.89 173.22,-25.75 172.37,-26.59 171.48,-27.41 170.56,-28.2 169.6,-28.96 168.61,-29.69 167.59,-30.39 166.54,-31.06 165.48,-31.69 164.39,-32.29 163.29,-32.84 162.18,-33.35 161.05,-33.82 159.91,-34.25 158.76,-34.64 157.61,-34.97 156.45,-35.26 155.28,-35.51 154.11,-35.7 152.94,-35.85 151.76,-35.95 150.59,-36 149.41,-36 148.24,-35.95 147.06,-35.85 145.89,-35.7 144.72,-35.51 143.55,-35.26 142.39,-34.97 141.24,-34.64 140.09,-34.25 138.95,-33.82 137.82,-33.35 136.71,-32.84 135.61,-32.29 134.52,-31.69 133.46,-31.06 132.41,-30.39 131.39,-29.69 130.4,-28.96 129.44,-28.2 128.52,-27.41 127.63,-26.59 126.78,-25.75 125.98,-24.89 125.23,-24.01 124.53,-23.11 123.89,-22.2 123.31,-21.28 122.79,-20.35 122.35,-19.41 121.97,-18.47 121.67,-17.53 121.45,-16.59 121.31,-15.65 121.26,-14.72 121.29,-13.8 121.41,-12.89 121.63,-11.99 121.93,-11.11 122.33,-10.25 122.82,-9.41 123.41,-8.59 124.09,-7.8 124.87,-7.04 125.74,-6.31 126.69,-5.61 127.74,-4.94 128.86,-4.31 130.07,-3.71 131.36,-3.16 132.72,-2.65 134.15,-2.18 135.64,-1.75 137.19,-1.36 138.79,-1.03 140.43,-0.74 142.12,-0.49 143.84,-0.3 145.58,-0.15 147.34,-0.05 149.11,0 150.89,0 152.66,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"150\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">t1</text>\n",
"</g>\n",
"<!-- t2 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>t2</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"53.68,-0.05 55.46,-0.15 57.22,-0.3 58.95,-0.49 60.65,-0.74 62.31,-1.03 63.92,-1.36 65.48,-1.75 66.99,-2.18 68.43,-2.65 69.8,-3.16 71.1,-3.71 72.32,-4.31 73.45,-4.94 74.51,-5.61 75.47,-6.31 76.35,-7.04 77.13,-7.8 77.81,-8.59 78.41,-9.41 78.91,-10.25 79.31,-11.11 79.62,-11.99 79.83,-12.89 79.96,-13.8 79.99,-14.72 79.93,-15.65 79.79,-16.59 79.57,-17.53 79.27,-18.47 78.89,-19.41 78.44,-20.35 77.92,-21.28 77.33,-22.2 76.69,-23.11 75.98,-24.01 75.22,-24.89 74.41,-25.75 73.56,-26.59 72.67,-27.41 71.73,-28.2 70.76,-28.96 69.76,-29.69 68.74,-30.39 67.68,-31.06 66.61,-31.69 65.52,-32.29 64.41,-32.84 63.28,-33.35 62.14,-33.82 60.99,-34.25 59.84,-34.64 58.67,-34.97 57.5,-35.26 56.33,-35.51 55.15,-35.7 53.96,-35.85 52.78,-35.95 51.59,-36 50.41,-36 49.22,-35.95 48.04,-35.85 46.85,-35.7 45.67,-35.51 44.5,-35.26 43.33,-34.97 42.16,-34.64 41.01,-34.25 39.86,-33.82 38.72,-33.35 37.59,-32.84 36.48,-32.29 35.39,-31.69 34.32,-31.06 33.26,-30.39 32.24,-29.69 31.24,-28.96 30.27,-28.2 29.33,-27.41 28.44,-26.59 27.59,-25.75 26.78,-24.89 26.02,-24.01 25.31,-23.11 24.67,-22.2 24.08,-21.28 23.56,-20.35 23.11,-19.41 22.73,-18.47 22.43,-17.53 22.21,-16.59 22.07,-15.65 22.01,-14.72 22.04,-13.8 22.17,-12.89 22.38,-11.99 22.69,-11.11 23.09,-10.25 23.59,-9.41 24.19,-8.59 24.87,-7.8 25.65,-7.04 26.53,-6.31 27.49,-5.61 28.55,-4.94 29.68,-4.31 30.9,-3.71 32.2,-3.16 33.57,-2.65 35.01,-2.18 36.52,-1.75 38.08,-1.36 39.69,-1.03 41.35,-0.74 43.05,-0.49 44.78,-0.3 46.54,-0.15 48.32,-0.05 50.1,0 51.9,0 53.68,-0.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"51\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">t2</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"53.66,-0.05 55.42,-0.15 57.16,-0.3 58.88,-0.49 60.57,-0.74 62.21,-1.03 63.81,-1.36 65.36,-1.75 66.85,-2.18 68.28,-2.65 69.64,-3.16 70.93,-3.71 72.14,-4.31 73.26,-4.94 74.31,-5.61 75.26,-6.31 76.13,-7.04 76.91,-7.8 77.59,-8.59 78.18,-9.41 78.67,-10.25 79.07,-11.11 79.37,-11.99 79.59,-12.89 79.71,-13.8 79.74,-14.72 79.69,-15.65 79.55,-16.59 79.33,-17.53 79.03,-18.47 78.65,-19.41 78.21,-20.35 77.69,-21.28 77.11,-22.2 76.47,-23.11 75.77,-24.01 75.02,-24.89 74.22,-25.75 73.37,-26.59 72.48,-27.41 71.56,-28.2 70.6,-28.96 69.61,-29.69 68.59,-30.39 67.54,-31.06 66.48,-31.69 65.39,-32.29 64.29,-32.84 63.18,-33.35 62.05,-33.82 60.91,-34.25 59.76,-34.64 58.61,-34.97 57.45,-35.26 56.28,-35.51 55.11,-35.7 53.94,-35.85 52.76,-35.95 51.59,-36 50.41,-36 49.24,-35.95 48.06,-35.85 46.89,-35.7 45.72,-35.51 44.55,-35.26 43.39,-34.97 42.24,-34.64 41.09,-34.25 39.95,-33.82 38.82,-33.35 37.71,-32.84 36.61,-32.29 35.52,-31.69 34.46,-31.06 33.41,-30.39 32.39,-29.69 31.4,-28.96 30.44,-28.2 29.52,-27.41 28.63,-26.59 27.78,-25.75 26.98,-24.89 26.23,-24.01 25.53,-23.11 24.89,-22.2 24.31,-21.28 23.79,-20.35 23.35,-19.41 22.97,-18.47 22.67,-17.53 22.45,-16.59 22.31,-15.65 22.26,-14.72 22.29,-13.8 22.41,-12.89 22.63,-11.99 22.93,-11.11 23.33,-10.25 23.82,-9.41 24.41,-8.59 25.09,-7.8 25.87,-7.04 26.74,-6.31 27.69,-5.61 28.74,-4.94 29.86,-4.31 31.07,-3.71 32.36,-3.16 33.72,-2.65 35.15,-2.18 36.64,-1.75 38.19,-1.36 39.79,-1.03 41.43,-0.74 43.12,-0.49 44.84,-0.3 46.58,-0.15 48.34,-0.05 50.11,0 51.89,0 53.66,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"51\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">t2</text>\n",
"</g>\n",
"<!-- z1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>z1</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"103.68,-174.05 105.46,-174.15 107.22,-174.3 108.95,-174.49 110.65,-174.74 112.31,-175.03 113.92,-175.36 115.48,-175.75 116.99,-176.18 118.43,-176.65 119.8,-177.16 121.1,-177.71 122.32,-178.31 123.45,-178.94 124.51,-179.61 125.47,-180.31 126.35,-181.04 127.13,-181.8 127.81,-182.59 128.41,-183.41 128.91,-184.25 129.31,-185.11 129.62,-185.99 129.83,-186.89 129.96,-187.8 129.99,-188.72 129.93,-189.65 129.79,-190.59 129.57,-191.53 129.27,-192.47 128.89,-193.41 128.44,-194.35 127.92,-195.28 127.33,-196.2 126.69,-197.11 125.98,-198.01 125.22,-198.89 124.41,-199.75 123.56,-200.59 122.67,-201.41 121.73,-202.2 120.76,-202.96 119.76,-203.69 118.74,-204.39 117.68,-205.06 116.61,-205.69 115.52,-206.29 114.41,-206.84 113.28,-207.35 112.14,-207.82 110.99,-208.25 109.84,-208.64 108.67,-208.97 107.5,-209.26 106.33,-209.51 105.15,-209.7 103.96,-209.85 102.78,-209.95 101.59,-210 100.41,-210 99.22,-209.95 98.04,-209.85 96.85,-209.7 95.67,-209.51 94.5,-209.26 93.33,-208.97 92.16,-208.64 91.01,-208.25 89.86,-207.82 88.72,-207.35 87.59,-206.84 86.48,-206.29 85.39,-205.69 84.32,-205.06 83.26,-204.39 82.24,-203.69 81.24,-202.96 80.27,-202.2 79.33,-201.41 78.44,-200.59 77.59,-199.75 76.78,-198.89 76.02,-198.01 75.31,-197.11 74.67,-196.2 74.08,-195.28 73.56,-194.35 73.11,-193.41 72.73,-192.47 72.43,-191.53 72.21,-190.59 72.07,-189.65 72.01,-188.72 72.04,-187.8 72.17,-186.89 72.38,-185.99 72.69,-185.11 73.09,-184.25 73.59,-183.41 74.19,-182.59 74.87,-181.8 75.65,-181.04 76.53,-180.31 77.49,-179.61 78.55,-178.94 79.68,-178.31 80.9,-177.71 82.2,-177.16 83.57,-176.65 85.01,-176.18 86.52,-175.75 88.08,-175.36 89.69,-175.03 91.35,-174.74 93.05,-174.49 94.78,-174.3 96.54,-174.15 98.32,-174.05 100.1,-174 101.9,-174 103.68,-174.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"101\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">z1</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"103.66,-177.05 105.42,-177.15 107.16,-177.3 108.88,-177.49 110.57,-177.74 112.21,-178.03 113.81,-178.36 115.36,-178.75 116.85,-179.18 118.28,-179.65 119.64,-180.16 120.93,-180.71 122.14,-181.31 123.26,-181.94 124.31,-182.61 125.26,-183.31 126.13,-184.04 126.91,-184.8 127.59,-185.59 128.18,-186.41 128.67,-187.25 129.07,-188.11 129.37,-188.99 129.59,-189.89 129.71,-190.8 129.74,-191.72 129.69,-192.65 129.55,-193.59 129.33,-194.53 129.03,-195.47 128.65,-196.41 128.21,-197.35 127.69,-198.28 127.11,-199.2 126.47,-200.11 125.77,-201.01 125.02,-201.89 124.22,-202.75 123.37,-203.59 122.48,-204.41 121.56,-205.2 120.6,-205.96 119.61,-206.69 118.59,-207.39 117.54,-208.06 116.48,-208.69 115.39,-209.29 114.29,-209.84 113.18,-210.35 112.05,-210.82 110.91,-211.25 109.76,-211.64 108.61,-211.97 107.45,-212.26 106.28,-212.51 105.11,-212.7 103.94,-212.85 102.76,-212.95 101.59,-213 100.41,-213 99.24,-212.95 98.06,-212.85 96.89,-212.7 95.72,-212.51 94.55,-212.26 93.39,-211.97 92.24,-211.64 91.09,-211.25 89.95,-210.82 88.82,-210.35 87.71,-209.84 86.61,-209.29 85.52,-208.69 84.46,-208.06 83.41,-207.39 82.39,-206.69 81.4,-205.96 80.44,-205.2 79.52,-204.41 78.63,-203.59 77.78,-202.75 76.98,-201.89 76.23,-201.01 75.53,-200.11 74.89,-199.2 74.31,-198.28 73.79,-197.35 73.35,-196.41 72.97,-195.47 72.67,-194.53 72.45,-193.59 72.31,-192.65 72.26,-191.72 72.29,-190.8 72.41,-189.89 72.63,-188.99 72.93,-188.11 73.33,-187.25 73.82,-186.41 74.41,-185.59 75.09,-184.8 75.87,-184.04 76.74,-183.31 77.69,-182.61 78.74,-181.94 79.86,-181.31 81.07,-180.71 82.36,-180.16 83.72,-179.65 85.15,-179.18 86.64,-178.75 88.19,-178.36 89.79,-178.03 91.43,-177.74 93.12,-177.49 94.84,-177.3 96.58,-177.15 98.34,-177.05 100.11,-177 101.89,-177 103.66,-177.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"101\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">z1</text>\n",
"</g>\n",
"<!-- z2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>z2</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"251.68,-174.05 253.46,-174.15 255.22,-174.3 256.95,-174.49 258.65,-174.74 260.31,-175.03 261.92,-175.36 263.48,-175.75 264.99,-176.18 266.43,-176.65 267.8,-177.16 269.1,-177.71 270.32,-178.31 271.45,-178.94 272.51,-179.61 273.47,-180.31 274.35,-181.04 275.13,-181.8 275.81,-182.59 276.41,-183.41 276.91,-184.25 277.31,-185.11 277.62,-185.99 277.83,-186.89 277.96,-187.8 277.99,-188.72 277.93,-189.65 277.79,-190.59 277.57,-191.53 277.27,-192.47 276.89,-193.41 276.44,-194.35 275.92,-195.28 275.33,-196.2 274.69,-197.11 273.98,-198.01 273.22,-198.89 272.41,-199.75 271.56,-200.59 270.67,-201.41 269.73,-202.2 268.76,-202.96 267.76,-203.69 266.74,-204.39 265.68,-205.06 264.61,-205.69 263.52,-206.29 262.41,-206.84 261.28,-207.35 260.14,-207.82 258.99,-208.25 257.84,-208.64 256.67,-208.97 255.5,-209.26 254.33,-209.51 253.15,-209.7 251.96,-209.85 250.78,-209.95 249.59,-210 248.41,-210 247.22,-209.95 246.04,-209.85 244.85,-209.7 243.67,-209.51 242.5,-209.26 241.33,-208.97 240.16,-208.64 239.01,-208.25 237.86,-207.82 236.72,-207.35 235.59,-206.84 234.48,-206.29 233.39,-205.69 232.32,-205.06 231.26,-204.39 230.24,-203.69 229.24,-202.96 228.27,-202.2 227.33,-201.41 226.44,-200.59 225.59,-199.75 224.78,-198.89 224.02,-198.01 223.31,-197.11 222.67,-196.2 222.08,-195.28 221.56,-194.35 221.11,-193.41 220.73,-192.47 220.43,-191.53 220.21,-190.59 220.07,-189.65 220.01,-188.72 220.04,-187.8 220.17,-186.89 220.38,-185.99 220.69,-185.11 221.09,-184.25 221.59,-183.41 222.19,-182.59 222.87,-181.8 223.65,-181.04 224.53,-180.31 225.49,-179.61 226.55,-178.94 227.68,-178.31 228.9,-177.71 230.2,-177.16 231.57,-176.65 233.01,-176.18 234.52,-175.75 236.08,-175.36 237.69,-175.03 239.35,-174.74 241.05,-174.49 242.78,-174.3 244.54,-174.15 246.32,-174.05 248.1,-174 249.9,-174 251.68,-174.05\"/>\n",
- "<text text-anchor=\"middle\" x=\"249\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">z2</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"251.66,-177.05 253.42,-177.15 255.16,-177.3 256.88,-177.49 258.57,-177.74 260.21,-178.03 261.81,-178.36 263.36,-178.75 264.85,-179.18 266.28,-179.65 267.64,-180.16 268.93,-180.71 270.14,-181.31 271.26,-181.94 272.31,-182.61 273.26,-183.31 274.13,-184.04 274.91,-184.8 275.59,-185.59 276.18,-186.41 276.67,-187.25 277.07,-188.11 277.37,-188.99 277.59,-189.89 277.71,-190.8 277.74,-191.72 277.69,-192.65 277.55,-193.59 277.33,-194.53 277.03,-195.47 276.65,-196.41 276.21,-197.35 275.69,-198.28 275.11,-199.2 274.47,-200.11 273.77,-201.01 273.02,-201.89 272.22,-202.75 271.37,-203.59 270.48,-204.41 269.56,-205.2 268.6,-205.96 267.61,-206.69 266.59,-207.39 265.54,-208.06 264.48,-208.69 263.39,-209.29 262.29,-209.84 261.18,-210.35 260.05,-210.82 258.91,-211.25 257.76,-211.64 256.61,-211.97 255.45,-212.26 254.28,-212.51 253.11,-212.7 251.94,-212.85 250.76,-212.95 249.59,-213 248.41,-213 247.24,-212.95 246.06,-212.85 244.89,-212.7 243.72,-212.51 242.55,-212.26 241.39,-211.97 240.24,-211.64 239.09,-211.25 237.95,-210.82 236.82,-210.35 235.71,-209.84 234.61,-209.29 233.52,-208.69 232.46,-208.06 231.41,-207.39 230.39,-206.69 229.4,-205.96 228.44,-205.2 227.52,-204.41 226.63,-203.59 225.78,-202.75 224.98,-201.89 224.23,-201.01 223.53,-200.11 222.89,-199.2 222.31,-198.28 221.79,-197.35 221.35,-196.41 220.97,-195.47 220.67,-194.53 220.45,-193.59 220.31,-192.65 220.26,-191.72 220.29,-190.8 220.41,-189.89 220.63,-188.99 220.93,-188.11 221.33,-187.25 221.82,-186.41 222.41,-185.59 223.09,-184.8 223.87,-184.04 224.74,-183.31 225.69,-182.61 226.74,-181.94 227.86,-181.31 229.07,-180.71 230.36,-180.16 231.72,-179.65 233.15,-179.18 234.64,-178.75 236.19,-178.36 237.79,-178.03 239.43,-177.74 241.12,-177.49 242.84,-177.3 244.58,-177.15 246.34,-177.05 248.11,-177 249.89,-177 251.66,-177.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"249\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">z2</text>\n",
"</g>\n",
"<!-- not(t1) -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>not(t1)</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"158,-123 104,-123 104,-87 158,-87 158,-123\"/>\n",
- "<text text-anchor=\"middle\" x=\"131\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"158,-124.5 104,-124.5 104,-88.5 158,-88.5 158,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"131\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(t1)->t1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>not(t1)->t1</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M134.84,-86.8C137.46,-75.09 140.98,-59.34 143.97,-45.97\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"147.46,-46.41 146.23,-35.89 140.63,-44.88 147.46,-46.41\"/>\n",
- "<text text-anchor=\"middle\" x=\"144.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M134.75,-88.41C137.33,-76.68 140.81,-60.84 143.79,-47.25\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"147.2,-48.05 145.93,-37.53 140.37,-46.55 147.2,-48.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"145.38\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- not(t2) -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>not(t2)</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"86,-123 32,-123 32,-87 86,-87 86,-123\"/>\n",
- "<text text-anchor=\"middle\" x=\"59\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"86,-124.5 32,-124.5 32,-88.5 86,-88.5 86,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"59\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(t2)->t2 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>not(t2)->t2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M57.38,-86.8C56.29,-75.16 54.82,-59.55 53.56,-46.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"57.04,-45.8 52.62,-36.18 50.07,-46.46 57.04,-45.8\"/>\n",
- "<text text-anchor=\"middle\" x=\"59.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M57.42,-88.41C56.34,-76.76 54.89,-61.05 53.64,-47.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"57.15,-47.49 52.74,-37.86 50.18,-48.14 57.15,-47.49\"/>\n",
+ "<text text-anchor=\"middle\" x=\"59.38\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- not(z2) -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>not(z2)</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"275,-297 221,-297 221,-261 275,-261 275,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"248\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"275,-301.5 221,-301.5 221,-265.5 275,-265.5 275,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"248\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(z2)->z2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>not(z2)->z2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M248.2,-260.8C248.34,-249.16 248.52,-233.55 248.68,-220.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"252.18,-220.22 248.8,-210.18 245.18,-220.13 252.18,-220.22\"/>\n",
- "<text text-anchor=\"middle\" x=\"251.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M248.2,-265.41C248.33,-253.76 248.51,-238.05 248.67,-224.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"252.17,-224.9 248.78,-214.86 245.17,-224.82 252.17,-224.9\"/>\n",
+ "<text text-anchor=\"middle\" x=\"251.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- and(not(t1),t2) -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>and(not(t1),t2)</title>\n",
- "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"54,-210 0,-210 0,-174 54,-174 54,-210\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"54,-213 0,-213 0,-177 54,-177 54,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-188.45\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- and(not(t1),t2)->t2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>and(not(t1),t2)->t2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M21.65,-173.83C15.97,-153.02 8.73,-117 16,-87 19.76,-71.47 27.72,-55.52 35.1,-42.97\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"38.29,-44.45 40.55,-34.1 32.33,-40.79 38.29,-44.45\"/>\n",
- "<text text-anchor=\"middle\" x=\"19.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M21.74,-176.59C16.16,-155.49 9.06,-118.96 16.25,-88.5 19.91,-73.01 27.57,-57.04 34.78,-44.32\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"37.75,-46.17 39.85,-35.78 31.73,-42.59 37.75,-46.17\"/>\n",
+ "<text text-anchor=\"middle\" x=\"20.38\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- and(not(t1),t2)->not(t1) -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>and(not(t1),t2)->not(t1)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M54.12,-174.52C62.65,-168.96 71.94,-162.51 80,-156 89.7,-148.16 99.64,-138.77 108.15,-130.25\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"110.71,-132.64 115.21,-123.05 105.71,-127.74 110.71,-132.64\"/>\n",
- "<text text-anchor=\"middle\" x=\"100.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M54.45,-177.41C62.91,-171.9 72.07,-165.5 80,-159 89.63,-151.1 99.44,-141.61 107.85,-132.94\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"110.35,-135.39 114.69,-125.73 105.27,-130.57 110.35,-135.39\"/>\n",
+ "<text text-anchor=\"middle\" x=\"101.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))) -->\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"151,-471 97,-471 97,-435 151,-435 151,-471\"/>\n",
- "<text text-anchor=\"middle\" x=\"124\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"151,-478.5 97,-478.5 97,-442.5 151,-442.5 151,-478.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"124\" y=\"-453.95\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))) -->\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"115,-384 61,-384 61,-348 115,-348 115,-384\"/>\n",
- "<text text-anchor=\"middle\" x=\"88\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"115,-390 61,-390 61,-354 115,-354 115,-390\"/>\n",
+ "<text text-anchor=\"middle\" x=\"88\" y=\"-365.45\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))->and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))) -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))->and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M116.71,-434.8C111.69,-422.93 104.91,-406.93 99.2,-393.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"102.4,-392.02 95.27,-384.18 95.95,-394.75 102.4,-392.02\"/>\n",
- "<text text-anchor=\"middle\" x=\"112.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M116.89,-442.41C111.94,-430.52 105.23,-414.41 99.53,-400.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"102.88,-399.64 95.8,-391.75 96.41,-402.32 102.88,-399.64\"/>\n",
+ "<text text-anchor=\"middle\" x=\"113.38\" y=\"-411.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(z1,not(z2)) -->\n",
"<g id=\"node12\" class=\"node\">\n",
"<title>equiv(z1,not(z2))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"187,-384 133,-384 133,-348 187,-348 187,-384\"/>\n",
- "<text text-anchor=\"middle\" x=\"160\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"187,-390 133,-390 133,-354 187,-354 187,-390\"/>\n",
+ "<text text-anchor=\"middle\" x=\"160\" y=\"-365.45\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
"</g>\n",
"<!-- and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))->equiv(z1,not(z2)) -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))->equiv(z1,not(z2))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M131.29,-434.8C136.31,-422.93 143.09,-406.93 148.8,-393.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"152.05,-394.75 152.73,-384.18 145.6,-392.02 152.05,-394.75\"/>\n",
- "<text text-anchor=\"middle\" x=\"147.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M131.11,-442.41C136.06,-430.52 142.77,-414.41 148.47,-400.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"151.59,-402.32 152.2,-391.75 145.12,-399.64 151.59,-402.32\"/>\n",
+ "<text text-anchor=\"middle\" x=\"148.38\" y=\"-411.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(z1,and(not(t1),t2)) -->\n",
"<g id=\"node13\" class=\"node\">\n",
"<title>equiv(z1,and(not(t1),t2))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"88,-297 34,-297 34,-261 88,-261 88,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"61\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"88,-301.5 34,-301.5 34,-265.5 88,-265.5 88,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"61\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
"</g>\n",
"<!-- and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))->equiv(z1,and(not(t1),t2)) -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))->equiv(z1,and(not(t1),t2))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M82.54,-347.8C78.8,-336.05 73.78,-320.24 69.53,-306.84\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"72.82,-305.65 66.46,-297.18 66.15,-307.77 72.82,-305.65\"/>\n",
- "<text text-anchor=\"middle\" x=\"80.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M82.67,-353.91C78.99,-342.14 74.03,-326.23 69.77,-312.61\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"73.19,-311.8 66.87,-303.29 66.51,-313.88 73.19,-311.8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"80.38\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(z2,equiv(t1,not(t2))) -->\n",
"<g id=\"node14\" class=\"node\">\n",
"<title>equiv(z2,equiv(t1,not(t2)))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"203,-297 149,-297 149,-261 203,-261 203,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"176\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"203,-301.5 149,-301.5 149,-265.5 203,-265.5 203,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"176\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
"</g>\n",
"<!-- and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))->equiv(z2,equiv(t1,not(t2))) -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))->equiv(z2,equiv(t1,not(t2)))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M105.81,-347.8C118.69,-335.36 136.28,-318.36 150.63,-304.5\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"153.46,-306.64 158.22,-297.18 148.59,-301.61 153.46,-306.64\"/>\n",
- "<text text-anchor=\"middle\" x=\"140.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M105.39,-353.91C118.2,-341.32 135.83,-323.98 150.28,-309.79\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"152.59,-312.42 157.27,-302.91 147.68,-307.43 152.59,-312.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"142.38\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(t1,not(t2)) -->\n",
"<g id=\"node11\" class=\"node\">\n",
"<title>equiv(t1,not(t2))</title>\n",
- "<polygon fill=\"olive\" stroke=\"black\" points=\"202,-210 148,-210 148,-174 202,-174 202,-210\"/>\n",
- "<text text-anchor=\"middle\" x=\"175\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"202,-213 148,-213 148,-177 202,-177 202,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"175\" y=\"-188.45\" font-family=\"Times,serif\" font-size=\"14.00\">⟺</text>\n",
"</g>\n",
"<!-- equiv(t1,not(t2))->t1 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>equiv(t1,not(t2))->t1</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M174.57,-173.96C173.84,-153.28 171.93,-117.39 167,-87 164.75,-73.11 161.06,-57.9 157.7,-45.39\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"161.03,-44.31 154.98,-35.6 154.28,-46.18 161.03,-44.31\"/>\n",
- "<text text-anchor=\"middle\" x=\"174.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M174.56,-176.72C173.82,-155.74 171.91,-119.34 167,-88.5 164.79,-74.6 161.2,-59.39 157.9,-46.75\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"161.37,-46.18 155.38,-37.44 154.61,-48.01 161.37,-46.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"174.38\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(t1,not(t2))->not(t2) -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>equiv(t1,not(t2))->not(t2)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M147.7,-177.49C144.79,-176.24 141.85,-175.05 139,-174 110.05,-163.37 93.71,-177.89 72,-156 66.05,-150 62.72,-141.64 60.88,-133.48\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"64.31,-132.75 59.28,-123.43 57.4,-133.86 64.31,-132.75\"/>\n",
- "<text text-anchor=\"middle\" x=\"75.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M147.7,-180.49C144.79,-179.24 141.85,-178.05 139,-177 110.16,-166.4 93.85,-180.85 72.25,-159 66.25,-152.93 62.86,-144.53 60.97,-136.27\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"64.43,-135.78 59.42,-126.45 57.52,-136.87 64.43,-135.78\"/>\n",
+ "<text text-anchor=\"middle\" x=\"76.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(z1,not(z2))->z1 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>equiv(z1,not(z2))->z1</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M147.74,-347.76C144.23,-342.27 140.65,-336.05 138,-330 121.97,-293.37 111.4,-248.14 105.8,-219.92\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"109.22,-219.15 103.9,-209.99 102.35,-220.47 109.22,-219.15\"/>\n",
- "<text text-anchor=\"middle\" x=\"128.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M147.72,-353.77C144.21,-348.28 140.63,-342.06 138,-336 121.87,-298.88 111.4,-253.07 105.84,-224.19\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"109.29,-223.61 104.04,-214.41 102.41,-224.88 109.29,-223.61\"/>\n",
+ "<text text-anchor=\"middle\" x=\"127.38\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(z1,not(z2))->not(z2) -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>equiv(z1,not(z2))->not(z2)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M177.81,-347.8C190.69,-335.36 208.28,-318.36 222.63,-304.5\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"225.46,-306.64 230.22,-297.18 220.59,-301.61 225.46,-306.64\"/>\n",
- "<text text-anchor=\"middle\" x=\"212.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M177.39,-353.91C190.2,-341.32 207.83,-323.98 222.28,-309.79\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"224.59,-312.42 229.27,-302.91 219.68,-307.43 224.59,-312.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"214.38\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(z1,and(not(t1),t2))->z1 -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>equiv(z1,and(not(t1),t2))->z1</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M69.09,-260.8C74.83,-248.62 82.61,-232.08 89.05,-218.39\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"92.37,-219.56 93.46,-209.03 86.03,-216.58 92.37,-219.56\"/>\n",
- "<text text-anchor=\"middle\" x=\"87.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M68.9,-265.41C74.51,-253.29 82.14,-236.78 88.56,-222.9\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"91.73,-224.39 92.75,-213.84 85.38,-221.45 91.73,-224.39\"/>\n",
+ "<text text-anchor=\"middle\" x=\"88.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(z1,and(not(t1),t2))->and(not(t1),t2) -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>equiv(z1,and(not(t1),t2))->and(not(t1),t2)</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M54.12,-260.8C49.42,-249.05 43.1,-233.24 37.74,-219.84\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"40.83,-218.16 33.87,-210.18 34.33,-220.76 40.83,-218.16\"/>\n",
- "<text text-anchor=\"middle\" x=\"50.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M54.28,-265.41C49.61,-253.52 43.28,-237.41 37.89,-223.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"41.29,-222.79 34.37,-214.76 34.77,-225.35 41.29,-222.79\"/>\n",
+ "<text text-anchor=\"middle\" x=\"51.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- equiv(z2,equiv(t1,not(t2)))->z2 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>equiv(z2,equiv(t1,not(t2)))->z2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M190.77,-260.8C202.06,-247.66 217.7,-229.45 229.93,-215.21\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"232.81,-217.22 236.67,-207.35 227.5,-212.66 232.81,-217.22\"/>\n",
- "<text text-anchor=\"middle\" x=\"219.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M190.42,-265.41C201.57,-252.2 217.12,-233.77 229.4,-219.23\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"231.8,-221.81 235.58,-211.91 226.45,-217.29 231.8,-221.81\"/>\n",
+ "<text text-anchor=\"middle\" x=\"222.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- equiv(z2,equiv(t1,not(t2)))->equiv(t1,not(t2)) -->\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>equiv(z2,equiv(t1,not(t2)))->equiv(t1,not(t2))</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M175.8,-260.8C175.66,-249.16 175.48,-233.55 175.32,-220.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"178.82,-220.13 175.2,-210.18 171.82,-220.22 178.82,-220.13\"/>\n",
- "<text text-anchor=\"middle\" x=\"178.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M175.8,-265.41C175.67,-253.76 175.49,-238.05 175.33,-224.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"178.83,-224.82 175.22,-214.86 171.83,-224.9 178.83,-224.82\"/>\n",
+ "<text text-anchor=\"middle\" x=\"178.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -2586,7 +3079,7 @@
},
{
"cell_type": "code",
- "execution_count": 58,
+ "execution_count": 68,
"id": "51d5630b",
"metadata": {
"vscode": {
@@ -2614,7 +3107,7 @@
},
{
"cell_type": "code",
- "execution_count": 59,
+ "execution_count": 69,
"id": "f843534d",
"metadata": {
"vscode": {
@@ -2638,7 +3131,7 @@
},
{
"cell_type": "code",
- "execution_count": 60,
+ "execution_count": 70,
"id": "3e0e951d",
"metadata": {
"vscode": {
@@ -2662,7 +3155,7 @@
},
{
"cell_type": "code",
- "execution_count": 61,
+ "execution_count": 71,
"id": "8199e19a",
"metadata": {
"vscode": {
@@ -2694,7 +3187,7 @@
},
{
"cell_type": "code",
- "execution_count": 62,
+ "execution_count": 72,
"id": "fae03e15",
"metadata": {
"vscode": {
@@ -2718,7 +3211,7 @@
},
{
"cell_type": "code",
- "execution_count": 63,
+ "execution_count": 73,
"id": "94b16168",
"metadata": {
"vscode": {
@@ -2742,7 +3235,7 @@
},
{
"cell_type": "code",
- "execution_count": 64,
+ "execution_count": 74,
"id": "a49ecd78",
"metadata": {
"vscode": {
@@ -2766,7 +3259,7 @@
},
{
"cell_type": "code",
- "execution_count": 65,
+ "execution_count": 75,
"id": "49caff90",
"metadata": {
"vscode": {
@@ -2798,7 +3291,7 @@
},
{
"cell_type": "code",
- "execution_count": 66,
+ "execution_count": 76,
"id": "c1766e98",
"metadata": {
"vscode": {
@@ -2822,7 +3315,7 @@
},
{
"cell_type": "code",
- "execution_count": 67,
+ "execution_count": 77,
"id": "0fd61d87",
"metadata": {
"vscode": {
@@ -2836,77 +3329,77 @@
"<?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",
+ "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\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",
+ "<svg width=\"177pt\" height=\"310pt\"\n",
+ " viewBox=\"0.00 0.00 177.00 309.50\" 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 305.5)\">\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-305.5 173,-305.5 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",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"54.66,-0.05 56.42,-0.15 58.16,-0.3 59.88,-0.49 61.57,-0.74 63.21,-1.03 64.81,-1.36 66.36,-1.75 67.85,-2.18 69.28,-2.65 70.64,-3.16 71.93,-3.71 73.14,-4.31 74.26,-4.94 75.31,-5.61 76.26,-6.31 77.13,-7.04 77.91,-7.8 78.59,-8.59 79.18,-9.41 79.67,-10.25 80.07,-11.11 80.37,-11.99 80.59,-12.89 80.71,-13.8 80.74,-14.72 80.69,-15.65 80.55,-16.59 80.33,-17.53 80.03,-18.47 79.65,-19.41 79.21,-20.35 78.69,-21.28 78.11,-22.2 77.47,-23.11 76.77,-24.01 76.02,-24.89 75.22,-25.75 74.37,-26.59 73.48,-27.41 72.56,-28.2 71.6,-28.96 70.61,-29.69 69.59,-30.39 68.54,-31.06 67.48,-31.69 66.39,-32.29 65.29,-32.84 64.18,-33.35 63.05,-33.82 61.91,-34.25 60.76,-34.64 59.61,-34.97 58.45,-35.26 57.28,-35.51 56.11,-35.7 54.94,-35.85 53.76,-35.95 52.59,-36 51.41,-36 50.24,-35.95 49.06,-35.85 47.89,-35.7 46.72,-35.51 45.55,-35.26 44.39,-34.97 43.24,-34.64 42.09,-34.25 40.95,-33.82 39.82,-33.35 38.71,-32.84 37.61,-32.29 36.52,-31.69 35.46,-31.06 34.41,-30.39 33.39,-29.69 32.4,-28.96 31.44,-28.2 30.52,-27.41 29.63,-26.59 28.78,-25.75 27.98,-24.89 27.23,-24.01 26.53,-23.11 25.89,-22.2 25.31,-21.28 24.79,-20.35 24.35,-19.41 23.97,-18.47 23.67,-17.53 23.45,-16.59 23.31,-15.65 23.26,-14.72 23.29,-13.8 23.41,-12.89 23.63,-11.99 23.93,-11.11 24.33,-10.25 24.82,-9.41 25.41,-8.59 26.09,-7.8 26.87,-7.04 27.74,-6.31 28.69,-5.61 29.74,-4.94 30.86,-4.31 32.07,-3.71 33.36,-3.16 34.72,-2.65 36.15,-2.18 37.64,-1.75 39.19,-1.36 40.79,-1.03 42.43,-0.74 44.12,-0.49 45.84,-0.3 47.58,-0.15 49.34,-0.05 51.11,0 52.89,0 54.66,-0.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"52\" y=\"-12.95\" 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=\"olive\" 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",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"70.66,-88.55 72.42,-88.65 74.16,-88.8 75.88,-88.99 77.57,-89.24 79.21,-89.53 80.81,-89.86 82.36,-90.25 83.85,-90.68 85.28,-91.15 86.64,-91.66 87.93,-92.21 89.14,-92.81 90.26,-93.44 91.31,-94.11 92.26,-94.81 93.13,-95.54 93.91,-96.3 94.59,-97.09 95.18,-97.91 95.67,-98.75 96.07,-99.61 96.37,-100.49 96.59,-101.39 96.71,-102.3 96.74,-103.22 96.69,-104.15 96.55,-105.09 96.33,-106.03 96.03,-106.97 95.65,-107.91 95.21,-108.85 94.69,-109.78 94.11,-110.7 93.47,-111.61 92.77,-112.51 92.02,-113.39 91.22,-114.25 90.37,-115.09 89.48,-115.91 88.56,-116.7 87.6,-117.46 86.61,-118.19 85.59,-118.89 84.54,-119.56 83.48,-120.19 82.39,-120.79 81.29,-121.34 80.18,-121.85 79.05,-122.32 77.91,-122.75 76.76,-123.14 75.61,-123.47 74.45,-123.76 73.28,-124.01 72.11,-124.2 70.94,-124.35 69.76,-124.45 68.59,-124.5 67.41,-124.5 66.24,-124.45 65.06,-124.35 63.89,-124.2 62.72,-124.01 61.55,-123.76 60.39,-123.47 59.24,-123.14 58.09,-122.75 56.95,-122.32 55.82,-121.85 54.71,-121.34 53.61,-120.79 52.52,-120.19 51.46,-119.56 50.41,-118.89 49.39,-118.19 48.4,-117.46 47.44,-116.7 46.52,-115.91 45.63,-115.09 44.78,-114.25 43.98,-113.39 43.23,-112.51 42.53,-111.61 41.89,-110.7 41.31,-109.78 40.79,-108.85 40.35,-107.91 39.97,-106.97 39.67,-106.03 39.45,-105.09 39.31,-104.15 39.26,-103.22 39.29,-102.3 39.41,-101.39 39.63,-100.49 39.93,-99.61 40.33,-98.75 40.82,-97.91 41.41,-97.09 42.09,-96.3 42.87,-95.54 43.74,-94.81 44.69,-94.11 45.74,-93.44 46.86,-92.81 48.07,-92.21 49.36,-91.66 50.72,-91.15 52.15,-90.68 53.64,-90.25 55.19,-89.86 56.79,-89.53 58.43,-89.24 60.12,-88.99 61.84,-88.8 63.58,-88.65 65.34,-88.55 67.11,-88.5 68.89,-88.5 70.66,-88.55\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-101.45\" 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\">¬</text>\n",
+ "<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-124.5 115,-124.5 115,-88.5 169,-88.5 169,-124.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"142\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
"</g>\n",
"<!-- not(p)->p -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>not(p)->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M124.22,-88.41C109.87,-74.62 89.6,-55.14 74.19,-40.33\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"76.92,-38.1 67.29,-33.69 72.07,-43.15 76.92,-38.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"108.38\" y=\"-57.2\" 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=\"olive\" 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\">∧</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"54,-301.5 0,-301.5 0,-265.5 54,-265.5 54,-301.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-276.95\" font-family=\"Times,serif\" font-size=\"14.00\">∧</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->p -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M25.6,-265.22C23.2,-231.15 19.52,-153 30,-88.5 32.31,-74.25 36.94,-58.9 41.35,-46.26\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"44.61,-47.54 44.75,-36.94 38.03,-45.13 44.61,-47.54\"/>\n",
+ "<text text-anchor=\"middle\" x=\"28.38\" y=\"-145.7\" 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=\"olive\" 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\">∨</text>\n",
+ "<polygon fill=\"olive\" stroke=\"black\" points=\"95,-213 41,-213 41,-177 95,-177 95,-213\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-188.45\" font-family=\"Times,serif\" font-size=\"14.00\">∨</text>\n",
"</g>\n",
"<!-- and(p,or(q,not(p)))->or(q,not(p)) -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>and(p,or(q,not(p)))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M35.1,-265.41C40.74,-253.52 48.37,-237.41 54.87,-223.7\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"58.01,-225.25 59.13,-214.72 51.68,-222.26 58.01,-225.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"54.38\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- or(q,not(p))->q -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M68,-176.91C68,-165.26 68,-149.55 68,-136.02\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"71.5,-136.36 68,-126.36 64.5,-136.36 71.5,-136.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"71.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- or(q,not(p))->not(p) -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>or(q,not(p))->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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M82.62,-176.91C93.19,-164.55 107.67,-147.63 119.68,-133.58\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"122.33,-135.87 126.17,-126 117.01,-131.32 122.33,-135.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"114.38\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -2959,7 +3452,11 @@
"cell_type": "code",
"execution_count": null,
"id": "5e50f3c7",
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
"outputs": [],
"source": []
}