diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index f81f348fd310938bddcbf8f31985fd6e236265ad..70c4aef1cdf2848df7e0b6df3985badc6b626a4d 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -21,7 +21,7 @@
"- (¬ a)\n",
"- (a ∧ b)\n",
"- (a ∨ b)\n",
- "- (a ⇒ b)\n",
+ "- (a → b)\n",
"- (a ⟺ b)\n",
"No other formulas are WFF.\n",
"\n",
@@ -44,7 +44,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 59,
"id": "964ebd52",
"metadata": {
"vscode": {
@@ -59,13 +59,13 @@
"wff --> \"(¬\",wff,\")\".\n",
"wff --> \"(\", wff, \"∧\", wff, \")\".\n",
"wff --> \"(\", wff, \"∨\", wff, \")\".\n",
- "wff --> \"(\", wff, \"⇒\", wff, \")\".\n",
+ "wff --> \"(\", wff, \"→\", wff, \")\".\n",
"wff --> \"(\", wff, \"⟺\", wff, \")\"."
]
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 2,
"id": "fc6823ad",
"metadata": {
"vscode": {
@@ -89,7 +89,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 3,
"id": "152289b6",
"metadata": {
"vscode": {
@@ -113,7 +113,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 4,
"id": "2c3dd1bf",
"metadata": {
"vscode": {
@@ -148,9 +148,9 @@
"- then come implication and equivalence.\n",
"\n",
"So instead of\n",
- "- (((¬ p) ∧ (¬ q)) ⇒ ((¬ p) ∨ (¬ q)))\n",
+ "- (((¬ p) ∧ (¬ q)) → ((¬ p) ∨ (¬ q)))\n",
"we can write\n",
- "- ¬ p ∧ ¬ q ⇒ ¬ p ∨ ¬ q\n",
+ "- ¬ p ∧ ¬ q → ¬ p ∨ ¬ q\n",
"\n",
"We will try not not mix conjunction/disjunction and implication/equivalence without parentheses.\n",
"We will also not try to improve our Prolog parser here to accomodate these precedences.\n",
@@ -168,7 +168,7 @@
},
{
"cell_type": "code",
- "execution_count": 64,
+ "execution_count": 5,
"id": "78163b60",
"metadata": {
"vscode": {
@@ -183,7 +183,7 @@
"wff(not(A)) --> \"(¬\",wff(A),\")\".\n",
"wff(and(A,B)) --> \"(\", wff(A), \"∧\", wff(B), \")\".\n",
"wff(or(A,B)) --> \"(\", wff(A), \"∨\", wff(B), \")\".\n",
- "wff(impl(A,B)) --> \"(\", wff(A), \"⇒\", wff(B), \")\".\n",
+ "wff(impl(A,B)) --> \"(\", wff(A), \"→\", wff(B), \")\".\n",
"wff(equiv(A,B)) --> \"(\", wff(A), \"⟺\", wff(B), \")\".\n",
"\n",
"parse_wff(String,Formula) :- wff(Formula,String,\"\")."
@@ -191,7 +191,7 @@
},
{
"cell_type": "code",
- "execution_count": 65,
+ "execution_count": 6,
"id": "6b9c3364",
"metadata": {
"vscode": {
@@ -215,7 +215,7 @@
},
{
"cell_type": "code",
- "execution_count": 66,
+ "execution_count": 7,
"id": "075dc3b2",
"metadata": {
"vscode": {
@@ -239,7 +239,7 @@
},
{
"cell_type": "code",
- "execution_count": 67,
+ "execution_count": 8,
"id": "338cb7dd",
"metadata": {
"vscode": {
@@ -273,7 +273,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 9,
"id": "f6116612",
"metadata": {
"vscode": {
@@ -297,7 +297,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 10,
"id": "d7e68593",
"metadata": {
"vscode": {
@@ -347,7 +347,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 11,
"id": "3646e3ee",
"metadata": {
"vscode": {
@@ -407,7 +407,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 12,
"id": "350b9756",
"metadata": {
"vscode": {
@@ -447,7 +447,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 13,
"id": "3101448b",
"metadata": {
"vscode": {
@@ -471,7 +471,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 14,
"id": "922004e9",
"metadata": {
"vscode": {
@@ -503,7 +503,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 15,
"id": "54b57ff8",
"metadata": {
"vscode": {
@@ -562,7 +562,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 16,
"id": "8f6d804b",
"metadata": {
"vscode": {
@@ -597,7 +597,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 17,
"id": "175c00d0",
"metadata": {
"vscode": {
@@ -630,7 +630,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 18,
"id": "eee17774",
"metadata": {
"vscode": {
@@ -662,7 +662,7 @@
},
{
"cell_type": "code",
- "execution_count": 68,
+ "execution_count": 19,
"id": "575fc20f",
"metadata": {
"vscode": {
@@ -1092,104 +1092,16 @@
"metadata": {},
"source": [
"\n",
- "Two formulas are called <b>equivalent</b> iff they have the same models:"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 29,
- "id": "b912acd3",
- "metadata": {
- "vscode": {
- "languageId": "prolog"
- }
- },
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "P | Q | Res | \n",
- ":- | :- | :- | \n",
- "true | true | true | \n",
- "true | false | false | \n",
- "false | true | true | \n",
- "false | false | true | "
- ],
- "text/plain": [
- "P | Q | Res | \n",
- ":- | :- | :- | \n",
- "true | true | true | \n",
- "true | false | false | \n",
- "false | true | true | \n",
- "false | false | true | "
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "\u001b[1mtrue"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- }
- ],
- "source": [
- "jupyter:print_table(value(or(not(p),q), [p/P, q/Q],Res))"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 30,
- "id": "f4c9823d",
- "metadata": {
- "vscode": {
- "languageId": "prolog"
- }
- },
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "P | Q | Res | \n",
- ":- | :- | :- | \n",
- "true | true | true | \n",
- "true | false | false | \n",
- "false | true | true | \n",
- "false | false | true | "
- ],
- "text/plain": [
- "P | Q | Res | \n",
- ":- | :- | :- | \n",
- "true | true | true | \n",
- "true | false | false | \n",
- "false | true | true | \n",
- "false | false | true | "
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "\u001b[1mtrue"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- }
- ],
- "source": [
- "jupyter:print_table(value(implies(p,q), [p/P, q/Q],Res))"
+ "Two formulas are called <b>equivalent</b> iff they have the same models.\n",
+ "We write this as `A ≡ B`.\n",
+ "\n",
+ "Below we can see that the models of `¬p ∨ q` and `p → q` are identical,\n",
+ "i.e., `¬p ∨ q ≡ p → q`."
]
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 31,
"id": "68a2a19c",
"metadata": {
"vscode": {
@@ -1238,7 +1150,11 @@
"id": "248d3d32",
"metadata": {},
"source": [
- "A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`:"
+ "A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`.\n",
+ "We write this as `A ⊨ B`.\n",
+ "\n",
+ "Below we can see that all models of `p ∧ q` are also models of `p ∨ q`,\n",
+ "i.e., `p ∧ q ⊨ p ∨ q`."
]
},
{
@@ -1300,7 +1216,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 33,
"id": "da0a82b5",
"metadata": {
"vscode": {
@@ -1322,7 +1238,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 34,
"id": "82980216",
"metadata": {
"vscode": {
@@ -1354,7 +1270,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 35,
"id": "23cfb806",
"metadata": {
"vscode": {
@@ -1376,7 +1292,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 36,
"id": "6338f6bf",
"metadata": {
"vscode": {
@@ -1400,7 +1316,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 37,
"id": "266a4bd8",
"metadata": {
"vscode": {
@@ -1436,7 +1352,7 @@
},
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": 38,
"id": "6957d9f3",
"metadata": {
"vscode": {
@@ -1453,7 +1369,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 39,
"id": "f552a71e",
"metadata": {
"vscode": {
@@ -1477,7 +1393,7 @@
},
{
"cell_type": "code",
- "execution_count": 48,
+ "execution_count": 40,
"id": "f8aca8b7",
"metadata": {
"vscode": {
@@ -1501,7 +1417,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": 41,
"id": "e7a2828d",
"metadata": {
"vscode": {
@@ -1533,7 +1449,7 @@
},
{
"cell_type": "code",
- "execution_count": 44,
+ "execution_count": 42,
"id": "26bab55b",
"metadata": {
"vscode": {
@@ -1548,7 +1464,7 @@
},
{
"cell_type": "code",
- "execution_count": 45,
+ "execution_count": 43,
"id": "fe5daeb4",
"metadata": {
"vscode": {
@@ -1587,7 +1503,7 @@
},
{
"cell_type": "code",
- "execution_count": 50,
+ "execution_count": 44,
"id": "3187bee7",
"metadata": {
"vscode": {
@@ -1619,7 +1535,7 @@
},
{
"cell_type": "code",
- "execution_count": 52,
+ "execution_count": 45,
"id": "df153b0a",
"metadata": {
"vscode": {
@@ -1656,7 +1572,7 @@
},
{
"cell_type": "code",
- "execution_count": 53,
+ "execution_count": 46,
"id": "4363c114",
"metadata": {
"vscode": {
@@ -1680,7 +1596,7 @@
},
{
"cell_type": "code",
- "execution_count": 54,
+ "execution_count": 47,
"id": "0919b40c",
"metadata": {
"vscode": {
@@ -1722,7 +1638,7 @@
},
{
"cell_type": "code",
- "execution_count": 55,
+ "execution_count": 48,
"id": "51d5630b",
"metadata": {
"vscode": {
@@ -1750,7 +1666,7 @@
},
{
"cell_type": "code",
- "execution_count": 56,
+ "execution_count": 49,
"id": "f843534d",
"metadata": {
"vscode": {
@@ -1774,7 +1690,7 @@
},
{
"cell_type": "code",
- "execution_count": 57,
+ "execution_count": 50,
"id": "3e0e951d",
"metadata": {
"vscode": {
@@ -1798,7 +1714,7 @@
},
{
"cell_type": "code",
- "execution_count": 58,
+ "execution_count": 51,
"id": "8199e19a",
"metadata": {
"vscode": {
@@ -1830,7 +1746,7 @@
},
{
"cell_type": "code",
- "execution_count": 60,
+ "execution_count": 52,
"id": "fae03e15",
"metadata": {
"vscode": {
@@ -1854,7 +1770,7 @@
},
{
"cell_type": "code",
- "execution_count": 61,
+ "execution_count": 53,
"id": "94b16168",
"metadata": {
"vscode": {
@@ -1878,7 +1794,7 @@
},
{
"cell_type": "code",
- "execution_count": 62,
+ "execution_count": 54,
"id": "a49ecd78",
"metadata": {
"vscode": {
@@ -1902,7 +1818,7 @@
},
{
"cell_type": "code",
- "execution_count": 63,
+ "execution_count": 55,
"id": "49caff90",
"metadata": {
"vscode": {
@@ -1924,15 +1840,92 @@
"?- generate_formula(Formula), equivalent(and(p,or(p,q)),Formula)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "c57cbe05",
+ "metadata": {},
+ "source": [
+ "Another side note: we can use the $Var feature of Jupyter Prolog to combine the parser and the show_graph feature:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 56,
+ "id": "c1766e98",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mFormula = and(p,or(q,not(p)))"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- parse_wff(\"(p∧(q∨(¬p)))\",Formula)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 58,
"id": "0fd61d87",
"metadata": {
"vscode": {
"languageId": "prolog"
}
},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"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",
+ "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)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"or(q,not(p))\" -> \"q\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"or(q,not(p))\" -> \"not(p)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ "}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:show_graph(subnode_val(_,_,$Formula,[p/true,q/true]),subtree/3)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "78693e86",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
"outputs": [],
"source": []
}