From 4c7d01610355b26e1c24542657f24c301677c5cc Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 25 Oct 2022 13:17:10 +0200
Subject: [PATCH] use unicode labels for trees
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
logic_programming/3_PropositionalLogic.ipynb | 268 ++++++++++++++-----
1 file changed, 198 insertions(+), 70 deletions(-)
diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 70c4aef..f8c5253 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -25,7 +25,7 @@
"- (a ⟺ b)\n",
"No other formulas are WFF.\n",
"\n",
- "Note in the slides we use the single arrow `→` instead of the double arrow `⇒` for implication.\n",
+ "Note in the slides we use the single arrow `→` instead of the double arrow `⇒` for implication which is maybe more standard.\n",
"\n",
"Comment: a, b are metavariablens outside the syntax of propositional logic.\n"
]
@@ -44,7 +44,7 @@
},
{
"cell_type": "code",
- "execution_count": 59,
+ "execution_count": 123,
"id": "964ebd52",
"metadata": {
"vscode": {
@@ -65,7 +65,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 124,
"id": "fc6823ad",
"metadata": {
"vscode": {
@@ -89,7 +89,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 125,
"id": "152289b6",
"metadata": {
"vscode": {
@@ -113,7 +113,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 126,
"id": "2c3dd1bf",
"metadata": {
"vscode": {
@@ -168,7 +168,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 127,
"id": "78163b60",
"metadata": {
"vscode": {
@@ -191,7 +191,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 128,
"id": "6b9c3364",
"metadata": {
"vscode": {
@@ -215,7 +215,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 129,
"id": "075dc3b2",
"metadata": {
"vscode": {
@@ -239,7 +239,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 130,
"id": "338cb7dd",
"metadata": {
"vscode": {
@@ -273,7 +273,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 131,
"id": "f6116612",
"metadata": {
"vscode": {
@@ -297,7 +297,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 132,
"id": "d7e68593",
"metadata": {
"vscode": {
@@ -347,7 +347,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 133,
"id": "3646e3ee",
"metadata": {
"vscode": {
@@ -407,7 +407,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 134,
"id": "350b9756",
"metadata": {
"vscode": {
@@ -447,7 +447,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 135,
"id": "3101448b",
"metadata": {
"vscode": {
@@ -471,7 +471,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 136,
"id": "922004e9",
"metadata": {
"vscode": {
@@ -503,7 +503,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 137,
"id": "54b57ff8",
"metadata": {
"vscode": {
@@ -562,7 +562,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 138,
"id": "8f6d804b",
"metadata": {
"vscode": {
@@ -597,7 +597,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 139,
"id": "175c00d0",
"metadata": {
"vscode": {
@@ -630,7 +630,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 140,
"id": "eee17774",
"metadata": {
"vscode": {
@@ -662,7 +662,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 141,
"id": "575fc20f",
"metadata": {
"vscode": {
@@ -696,7 +696,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 142,
"id": "fec75f65",
"metadata": {
"vscode": {
@@ -729,7 +729,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 143,
"id": "78473da0",
"metadata": {
"vscode": {
@@ -784,7 +784,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 144,
"id": "2ee60c15",
"metadata": {
"vscode": {
@@ -796,13 +796,20 @@
"\n",
"subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :- \n",
" rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering\n",
- " functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),\n",
- " (value(Sub,Interpretation,true) -> C=olive ; C=sienna1)."
+ " get_label(Sub,F), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),\n",
+ " (value(Sub,Interpretation,true) -> C=olive ; C=sienna1).\n",
+ "\n",
+ "get_label(and(_,_),'∧') :- !.\n",
+ "get_label(or(_,_),'∨') :- !.\n",
+ "get_label(impl(_,_),'→') :- !.\n",
+ "get_label(equiv(_,_),'⟺') :- !.\n",
+ "get_label(not(_),'¬') :- !.\n",
+ "get_label(Sub,F) :- functor(Sub,F,_)."
]
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 145,
"id": "2b497dad",
"metadata": {
"vscode": {
@@ -812,14 +819,14 @@
"outputs": [
{
"data": {
- "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"70.68,-87.05 72.46,-87.15 74.22,-87.3 75.95,-87.49 77.65,-87.74 79.31,-88.03 80.92,-88.36 82.48,-88.75 83.99,-89.18 85.43,-89.65 86.8,-90.16 88.1,-90.71 89.32,-91.31 90.45,-91.94 91.51,-92.61 92.47,-93.31 93.35,-94.04 94.13,-94.8 94.81,-95.59 95.41,-96.41 95.91,-97.25 96.31,-98.11 96.62,-98.99 96.83,-99.89 96.96,-100.8 96.99,-101.72 96.93,-102.65 96.79,-103.59 96.57,-104.53 96.27,-105.47 95.89,-106.41 95.44,-107.35 94.92,-108.28 94.33,-109.2 93.69,-110.11 92.98,-111.01 92.22,-111.89 91.41,-112.75 90.56,-113.59 89.67,-114.41 88.73,-115.2 87.76,-115.96 86.76,-116.69 85.74,-117.39 84.68,-118.06 83.61,-118.69 82.52,-119.29 81.41,-119.84 80.28,-120.35 79.14,-120.82 77.99,-121.25 76.84,-121.64 75.67,-121.97 74.5,-122.26 73.33,-122.51 72.15,-122.7 70.96,-122.85 69.78,-122.95 68.59,-123 67.41,-123 66.22,-122.95 65.04,-122.85 63.85,-122.7 62.67,-122.51 61.5,-122.26 60.33,-121.97 59.16,-121.64 58.01,-121.25 56.86,-120.82 55.72,-120.35 54.59,-119.84 53.48,-119.29 52.39,-118.69 51.32,-118.06 50.26,-117.39 49.24,-116.69 48.24,-115.96 47.27,-115.2 46.33,-114.41 45.44,-113.59 44.59,-112.75 43.78,-111.89 43.02,-111.01 42.31,-110.11 41.67,-109.2 41.08,-108.28 40.56,-107.35 40.11,-106.41 39.73,-105.47 39.43,-104.53 39.21,-103.59 39.07,-102.65 39.01,-101.72 39.04,-100.8 39.17,-99.89 39.38,-98.99 39.69,-98.11 40.09,-97.25 40.59,-96.41 41.19,-95.59 41.87,-94.8 42.65,-94.04 43.53,-93.31 44.49,-92.61 45.55,-91.94 46.68,-91.31 47.9,-90.71 49.2,-90.16 50.57,-89.65 52.01,-89.18 53.52,-88.75 55.08,-88.36 56.69,-88.03 58.35,-87.74 60.05,-87.49 61.78,-87.3 63.54,-87.15 65.32,-87.05 67.1,-87 68.9,-87 70.68,-87.05\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)->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</g>\n<!-- and(p,or(q,not(p))) -->\n<g id=\"node4\" class=\"node\">\n<title>and(p,or(q,not(p)))</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"54,-297 0,-297 0,-261 54,-261 54,-297\"/>\n<text text-anchor=\"middle\" x=\"27\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">and</text>\n</g>\n<!-- and(p,or(q,not(p)))->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</g>\n<!-- or(q,not(p)) -->\n<g id=\"node5\" class=\"node\">\n<title>or(q,not(p))</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"95,-210 41,-210 41,-174 95,-174 95,-210\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">or</text>\n</g>\n<!-- and(p,or(q,not(p)))->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</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</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</g>\n</g>\n</svg>\n",
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"70.68,-87.05 72.46,-87.15 74.22,-87.3 75.95,-87.49 77.65,-87.74 79.31,-88.03 80.92,-88.36 82.48,-88.75 83.99,-89.18 85.43,-89.65 86.8,-90.16 88.1,-90.71 89.32,-91.31 90.45,-91.94 91.51,-92.61 92.47,-93.31 93.35,-94.04 94.13,-94.8 94.81,-95.59 95.41,-96.41 95.91,-97.25 96.31,-98.11 96.62,-98.99 96.83,-99.89 96.96,-100.8 96.99,-101.72 96.93,-102.65 96.79,-103.59 96.57,-104.53 96.27,-105.47 95.89,-106.41 95.44,-107.35 94.92,-108.28 94.33,-109.2 93.69,-110.11 92.98,-111.01 92.22,-111.89 91.41,-112.75 90.56,-113.59 89.67,-114.41 88.73,-115.2 87.76,-115.96 86.76,-116.69 85.74,-117.39 84.68,-118.06 83.61,-118.69 82.52,-119.29 81.41,-119.84 80.28,-120.35 79.14,-120.82 77.99,-121.25 76.84,-121.64 75.67,-121.97 74.5,-122.26 73.33,-122.51 72.15,-122.7 70.96,-122.85 69.78,-122.95 68.59,-123 67.41,-123 66.22,-122.95 65.04,-122.85 63.85,-122.7 62.67,-122.51 61.5,-122.26 60.33,-121.97 59.16,-121.64 58.01,-121.25 56.86,-120.82 55.72,-120.35 54.59,-119.84 53.48,-119.29 52.39,-118.69 51.32,-118.06 50.26,-117.39 49.24,-116.69 48.24,-115.96 47.27,-115.2 46.33,-114.41 45.44,-113.59 44.59,-112.75 43.78,-111.89 43.02,-111.01 42.31,-110.11 41.67,-109.2 41.08,-108.28 40.56,-107.35 40.11,-106.41 39.73,-105.47 39.43,-104.53 39.21,-103.59 39.07,-102.65 39.01,-101.72 39.04,-100.8 39.17,-99.89 39.38,-98.99 39.69,-98.11 40.09,-97.25 40.59,-96.41 41.19,-95.59 41.87,-94.8 42.65,-94.04 43.53,-93.31 44.49,-92.61 45.55,-91.94 46.68,-91.31 47.9,-90.71 49.2,-90.16 50.57,-89.65 52.01,-89.18 53.52,-88.75 55.08,-88.36 56.69,-88.03 58.35,-87.74 60.05,-87.49 61.78,-87.3 63.54,-87.15 65.32,-87.05 67.1,-87 68.9,-87 70.68,-87.05\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">¬</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</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</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</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</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</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</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</g>\n</g>\n</svg>\n",
"text/plain": [
"digraph {\n",
"\"p\" [shape=\"egg\", label=\"p\", style=\"filled\", fillcolor=\"olive\"]\n",
"\"q\" [shape=\"egg\", label=\"q\", style=\"filled\", fillcolor=\"sienna1\"]\n",
- "\"not(p)\" [shape=\"rect\", label=\"not\", style=\"filled\", fillcolor=\"sienna1\"]\n",
- "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\", style=\"filled\", fillcolor=\"sienna1\"]\n",
- "\"or(q,not(p))\" [shape=\"rect\", label=\"or\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"not(p)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"or(q,not(p))\" [shape=\"rect\", label=\"∨\", style=\"filled\", fillcolor=\"sienna1\"]\n",
" \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
" \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
" \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
@@ -847,7 +854,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 146,
"id": "0fd23f05",
"metadata": {
"vscode": {
@@ -857,14 +864,14 @@
"outputs": [
{
"data": {
- "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"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</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)->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</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\">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</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\">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</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</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</g>\n</g>\n</svg>\n",
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"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</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</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</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</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</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</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</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</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</g>\n</g>\n</svg>\n",
"text/plain": [
"digraph {\n",
"\"p\" [shape=\"egg\", label=\"p\", style=\"filled\", fillcolor=\"olive\"]\n",
"\"q\" [shape=\"egg\", label=\"q\", style=\"filled\", fillcolor=\"olive\"]\n",
- "\"not(p)\" [shape=\"rect\", label=\"not\", style=\"filled\", fillcolor=\"sienna1\"]\n",
- "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\", style=\"filled\", fillcolor=\"olive\"]\n",
- "\"or(q,not(p))\" [shape=\"rect\", label=\"or\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"not(p)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"or(q,not(p))\" [shape=\"rect\", label=\"∨\", style=\"filled\", fillcolor=\"olive\"]\n",
" \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
" \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
" \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
@@ -900,7 +907,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 147,
"id": "23775624",
"metadata": {
"vscode": {
@@ -942,7 +949,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 148,
"id": "7a6e29ed",
"metadata": {
"vscode": {
@@ -996,7 +1003,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 149,
"id": "6bd292f4",
"metadata": {
"vscode": {
@@ -1053,7 +1060,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 150,
"id": "ab15628a",
"metadata": {
"vscode": {
@@ -1101,7 +1108,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 151,
"id": "68a2a19c",
"metadata": {
"vscode": {
@@ -1159,7 +1166,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 152,
"id": "aaf46953",
"metadata": {
"vscode": {
@@ -1216,7 +1223,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 153,
"id": "da0a82b5",
"metadata": {
"vscode": {
@@ -1238,7 +1245,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 154,
"id": "82980216",
"metadata": {
"vscode": {
@@ -1270,7 +1277,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 155,
"id": "23cfb806",
"metadata": {
"vscode": {
@@ -1292,7 +1299,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 156,
"id": "6338f6bf",
"metadata": {
"vscode": {
@@ -1316,7 +1323,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 157,
"id": "266a4bd8",
"metadata": {
"vscode": {
@@ -1352,7 +1359,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 158,
"id": "6957d9f3",
"metadata": {
"vscode": {
@@ -1369,7 +1376,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 159,
"id": "f552a71e",
"metadata": {
"vscode": {
@@ -1393,7 +1400,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 160,
"id": "f8aca8b7",
"metadata": {
"vscode": {
@@ -1417,7 +1424,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": 161,
"id": "e7a2828d",
"metadata": {
"vscode": {
@@ -1449,7 +1456,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 162,
"id": "26bab55b",
"metadata": {
"vscode": {
@@ -1464,7 +1471,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": 163,
"id": "fe5daeb4",
"metadata": {
"vscode": {
@@ -1503,7 +1510,7 @@
},
{
"cell_type": "code",
- "execution_count": 44,
+ "execution_count": 164,
"id": "3187bee7",
"metadata": {
"vscode": {
@@ -1535,7 +1542,7 @@
},
{
"cell_type": "code",
- "execution_count": 45,
+ "execution_count": 165,
"id": "df153b0a",
"metadata": {
"vscode": {
@@ -1557,6 +1564,60 @@
"?- prove(and(equiv(a,or(not(b),not(c))),equiv(b,a)), and(a,and(b,not(c))))."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 166,
+ "id": "1712e9e0",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"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<!-- 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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "digraph {\n",
+ "\"a\" [shape=\"egg\", label=\"a\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"b\" [shape=\"egg\", label=\"b\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"c\" [shape=\"egg\", label=\"c\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"not(b)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"not(c)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"and(equiv(a,or(not(b),not(c))),equiv(b,a))\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"equiv(a,or(not(b),not(c)))\" [shape=\"rect\", label=\"⟺\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"equiv(b,a)\" [shape=\"rect\", label=\"⟺\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"or(not(b),not(c))\" [shape=\"rect\", label=\"∨\", style=\"filled\", fillcolor=\"olive\"]\n",
+ " \"not(b)\" -> \"b\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"not(c)\" -> \"c\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(equiv(a,or(not(b),not(c))),equiv(b,a))\" -> \"equiv(a,or(not(b),not(c)))\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(equiv(a,or(not(b),not(c))),equiv(b,a))\" -> \"equiv(b,a)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(a,or(not(b),not(c)))\" -> \"a\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(a,or(not(b),not(c)))\" -> \"or(not(b),not(c))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(b,a)\" -> \"b\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(b,a)\" -> \"a\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"or(not(b),not(c))\" -> \"not(b)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"or(not(b),not(c))\" -> \"not(c)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ "}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:show_graph(subnode_val(_,_,and(equiv(a,or(not(b),not(c))),equiv(b,a)),[a/true,b/true,c/false]),subtree/3)."
+ ]
+ },
{
"cell_type": "markdown",
"id": "c0299ea9",
@@ -1572,7 +1633,7 @@
},
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": 167,
"id": "4363c114",
"metadata": {
"vscode": {
@@ -1596,7 +1657,7 @@
},
{
"cell_type": "code",
- "execution_count": 47,
+ "execution_count": 168,
"id": "0919b40c",
"metadata": {
"vscode": {
@@ -1618,6 +1679,73 @@
"jupyter:retry."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 169,
+ "id": "f64a00fe",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"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<!-- 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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</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</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "digraph {\n",
+ "\"t1\" [shape=\"egg\", label=\"t1\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"t2\" [shape=\"egg\", label=\"t2\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"z1\" [shape=\"egg\", label=\"z1\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"z2\" [shape=\"egg\", label=\"z2\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"not(t1)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"not(t2)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"not(z2)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"and(not(t1),t2)\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"equiv(t1,not(t2))\" [shape=\"rect\", label=\"⟺\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"equiv(z1,not(z2))\" [shape=\"rect\", label=\"⟺\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"equiv(z1,and(not(t1),t2))\" [shape=\"rect\", label=\"⟺\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"equiv(z2,equiv(t1,not(t2)))\" [shape=\"rect\", label=\"⟺\", style=\"filled\", fillcolor=\"olive\"]\n",
+ " \"not(t1)\" -> \"t1\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"not(t2)\" -> \"t2\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"not(z2)\" -> \"z2\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(not(t1),t2)\" -> \"not(t1)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(not(t1),t2)\" -> \"t2\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2)))))\" -> \"equiv(z1,not(z2))\" [label=\"1\", color=\"black\", style=\"solid\"]\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))))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))\" -> \"equiv(z1,and(not(t1),t2))\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))\" -> \"equiv(z2,equiv(t1,not(t2)))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(t1,not(t2))\" -> \"t1\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(t1,not(t2))\" -> \"not(t2)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(z1,not(z2))\" -> \"z1\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(z1,not(z2))\" -> \"not(z2)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(z1,and(not(t1),t2))\" -> \"z1\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(z1,and(not(t1),t2))\" -> \"and(not(t1),t2)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(z2,equiv(t1,not(t2)))\" -> \"z2\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"equiv(z2,equiv(t1,not(t2)))\" -> \"equiv(t1,not(t2))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ "}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:show_graph(subnode_val(_,_,and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))),\n",
+ " [t1/true,t2/false,z1/false,z2/true]),subtree/3)."
+ ]
+ },
{
"cell_type": "markdown",
"id": "35fba4c7",
@@ -1638,7 +1766,7 @@
},
{
"cell_type": "code",
- "execution_count": 48,
+ "execution_count": 170,
"id": "51d5630b",
"metadata": {
"vscode": {
@@ -1666,7 +1794,7 @@
},
{
"cell_type": "code",
- "execution_count": 49,
+ "execution_count": 171,
"id": "f843534d",
"metadata": {
"vscode": {
@@ -1690,7 +1818,7 @@
},
{
"cell_type": "code",
- "execution_count": 50,
+ "execution_count": 172,
"id": "3e0e951d",
"metadata": {
"vscode": {
@@ -1714,7 +1842,7 @@
},
{
"cell_type": "code",
- "execution_count": 51,
+ "execution_count": 173,
"id": "8199e19a",
"metadata": {
"vscode": {
@@ -1746,7 +1874,7 @@
},
{
"cell_type": "code",
- "execution_count": 52,
+ "execution_count": 174,
"id": "fae03e15",
"metadata": {
"vscode": {
@@ -1770,7 +1898,7 @@
},
{
"cell_type": "code",
- "execution_count": 53,
+ "execution_count": 175,
"id": "94b16168",
"metadata": {
"vscode": {
@@ -1794,7 +1922,7 @@
},
{
"cell_type": "code",
- "execution_count": 54,
+ "execution_count": 176,
"id": "a49ecd78",
"metadata": {
"vscode": {
@@ -1818,7 +1946,7 @@
},
{
"cell_type": "code",
- "execution_count": 55,
+ "execution_count": 177,
"id": "49caff90",
"metadata": {
"vscode": {
@@ -1850,7 +1978,7 @@
},
{
"cell_type": "code",
- "execution_count": 56,
+ "execution_count": 178,
"id": "c1766e98",
"metadata": {
"vscode": {
@@ -1874,7 +2002,7 @@
},
{
"cell_type": "code",
- "execution_count": 58,
+ "execution_count": 179,
"id": "0fd61d87",
"metadata": {
"vscode": {
@@ -1884,14 +2012,14 @@
"outputs": [
{
"data": {
- "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"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</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)->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</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\">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</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\">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</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</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</g>\n</g>\n</svg>\n",
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"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</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</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</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</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</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</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</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</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</g>\n</g>\n</svg>\n",
"text/plain": [
"digraph {\n",
"\"p\" [shape=\"egg\", label=\"p\", style=\"filled\", fillcolor=\"olive\"]\n",
"\"q\" [shape=\"egg\", label=\"q\", style=\"filled\", fillcolor=\"olive\"]\n",
- "\"not(p)\" [shape=\"rect\", label=\"not\", style=\"filled\", fillcolor=\"sienna1\"]\n",
- "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\", style=\"filled\", fillcolor=\"olive\"]\n",
- "\"or(q,not(p))\" [shape=\"rect\", label=\"or\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"not(p)\" [shape=\"rect\", label=\"¬\", style=\"filled\", fillcolor=\"sienna1\"]\n",
+ "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"∧\", style=\"filled\", fillcolor=\"olive\"]\n",
+ "\"or(q,not(p))\" [shape=\"rect\", label=\"∨\", style=\"filled\", fillcolor=\"olive\"]\n",
" \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
" \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
" \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
--
GitLab