{ "cells": [ { "cell_type": "markdown", "id": "9eb5530a", "metadata": {}, "source": [ "# Propositional Logic\n", "Syntax and Semantics Explained using a Prolog Implementation" ] }, { "cell_type": "markdown", "id": "dba70591", "metadata": {}, "source": [ "## Well-Formed Formulas (WFF)\n", "\n", "All atomic propositions are WFF)\n", "If a und b are WFF then so are:\n", "- (¬ a)\n", "- (a ∧ b)\n", "- (a ∨ b)\n", "- (a ⇒ b)\n", "- (a ⟺ b)\n", "No other formulas are WFF.\n", "\n", "Comment: a, b are metavariablens outside the syntax of propositional logic.\n" ] }, { "cell_type": "markdown", "id": "dd01f86a", "metadata": {}, "source": [ "Maybe this reminds you of formal grammars from a theoretical computer science lecture.\n", "And indeed, the above can be written as a grammar using a non-terminal symbol wff.\n", "\n", "In Prolog, grammars can actually be written using DCG notation, which we will see and understand much later in the course.\n", "Here we simply write the grammar in Prolog style and can then use it to check if a formula is a WFF:" ] }, { "cell_type": "code", "execution_count": 11, "id": "964ebd52", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1;31m% The Prolog server was restarted" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ " :- set_prolog_flag(double_quotes, codes).\n", "wff --> \"p\". % atomic proposition\n", "wff --> \"q\". % atomic proposition\n", "wff --> \"(¬\",wff,\")\".\n", "wff --> \"(\", wff, \"∧\", wff, \")\".\n", "wff --> \"(\", wff, \"∨\", wff, \")\".\n", "wff --> \"(\", wff, \"⇒\", wff, \")\".\n", "wff --> \"(\", wff, \"⟺\", wff, \")\"." ] }, { "cell_type": "code", "execution_count": 12, "id": "fc6823ad", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- wff(\"p\",\"\")." ] }, { "cell_type": "code", "execution_count": 13, "id": "152289b6", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- wff(\"(¬p)\",\"\")." ] }, { "cell_type": "code", "execution_count": 14, "id": "2c3dd1bf", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- wff(\"(p∧(q∨(¬p)))\",\"\").\n", "%comment." ] }, { "cell_type": "markdown", "id": "38b0a282", "metadata": {}, "source": [ "This grammar does not talk about whitespace and requires parentheses for every connective used.\n", "In practice, one typically uses operator precedences to avoid having to write too many parentheses:\n", "- negation binds strongest\n", "- then come conjunction and disjunction\n", "- then come implication and equivalence.\n", "\n", "So instead of\n", "- (((¬ p) ∧ (¬ q)) ⇒ ((¬ p) ∨ (¬ q)))\n", "we can write\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", "This is the subject of another course (on compiler construction)." ] }, { "cell_type": "markdown", "id": "92b6dc2d", "metadata": {}, "source": [ "We will also see much later that Prolog allows one to annotate grammars with semantic values, here to generate\n", "a Prolog term representing the logical formal in the form of a syntax tree:" ] }, { "cell_type": "code", "execution_count": 15, "id": "78163b60", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [ " :- set_prolog_flag(double_quotes, codes).\n", "wff(p) --> \"p\". % atomic proposition\n", "wff(q) --> \"q\". % atomic proposition\n", "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(equiv(A,B)) --> \"(\", wff(A), \"⟺\", wff(B), \")\"." ] }, { "cell_type": "code", "execution_count": 16, "id": "8ddb568d", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mFormula = not(p)" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- wff(Formula,\"(¬p)\",\"\")." ] }, { "cell_type": "code", "execution_count": 17, "id": "075dc3b2", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mFormula = not(and(p,q))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- wff(Formula,\"(¬(p∧q))\",\"\")." ] }, { "cell_type": "code", "execution_count": 18, "id": "338cb7dd", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mFormula = and(p,or(q,not(p)))" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- wff(Formula,\"(p∧(q∨(¬p)))\",\"\")." ] }, { "cell_type": "markdown", "id": "f9005519", "metadata": {}, "source": [ "The above Prolog term `and(p,or(q,not(p)))` represents the logical formula in tree form.\n", "We can display the tree as a dag (directed acyclic graph) using the following subsidiary code\n", "(in future the Jupyter kernel will probably have a dedicated command to show a term graphically):" ] }, { "cell_type": "code", "execution_count": 19, "id": "f6116612", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [ "subtree(Term,Nr,SubTerm) :- \n", " Term =.. [_|ArgList], %obtain arguments of the term\n", " nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number\n", "\n", "% recursive and transitive closure of subtree\n", "rec_subtree(Term,Sub) :- Term = Sub.\n", "rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub).\n", "\n", "subnode(Sub,[shape/S, label/F],Formula) :- \n", " rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering\n", " functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect)." ] }, { "cell_type": "code", "execution_count": 20, "id": "d7e68593", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/markdown": [ "Node | Dot | \n", ":- | :- | \n", "and(p,or(q,not(p))) | [shape/rect,label/and] | \n", "p | [shape/egg,label/p] | \n", "or(q,not(p)) | [shape/rect,label/or] | \n", "q | [shape/egg,label/q] | \n", "not(p) | [shape/rect,label/not] | \n", "p | [shape/egg,label/p] | " ], "text/plain": [ "Node | Dot | \n", ":- | :- | \n", "and(p,or(q,not(p))) | [shape/rect,label/and] | \n", "p | [shape/egg,label/p] | \n", "or(q,not(p)) | [shape/rect,label/or] | \n", "q | [shape/egg,label/q] | \n", "not(p) | [shape/rect,label/not] | \n", "p | [shape/egg,label/p] | " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p)))))" ] }, { "cell_type": "code", "execution_count": 21, "id": "3646e3ee", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"70.68,-87.05 72.46,-87.15 74.22,-87.3 75.95,-87.49 77.65,-87.74 79.31,-88.03 80.92,-88.36 82.48,-88.75 83.99,-89.18 85.43,-89.65 86.8,-90.16 88.1,-90.71 89.32,-91.31 90.45,-91.94 91.51,-92.61 92.47,-93.31 93.35,-94.04 94.13,-94.8 94.81,-95.59 95.41,-96.41 95.91,-97.25 96.31,-98.11 96.62,-98.99 96.83,-99.89 96.96,-100.8 96.99,-101.72 96.93,-102.65 96.79,-103.59 96.57,-104.53 96.27,-105.47 95.89,-106.41 95.44,-107.35 94.92,-108.28 94.33,-109.2 93.69,-110.11 92.98,-111.01 92.22,-111.89 91.41,-112.75 90.56,-113.59 89.67,-114.41 88.73,-115.2 87.76,-115.96 86.76,-116.69 85.74,-117.39 84.68,-118.06 83.61,-118.69 82.52,-119.29 81.41,-119.84 80.28,-120.35 79.14,-120.82 77.99,-121.25 76.84,-121.64 75.67,-121.97 74.5,-122.26 73.33,-122.51 72.15,-122.7 70.96,-122.85 69.78,-122.95 68.59,-123 67.41,-123 66.22,-122.95 65.04,-122.85 63.85,-122.7 62.67,-122.51 61.5,-122.26 60.33,-121.97 59.16,-121.64 58.01,-121.25 56.86,-120.82 55.72,-120.35 54.59,-119.84 53.48,-119.29 52.39,-118.69 51.32,-118.06 50.26,-117.39 49.24,-116.69 48.24,-115.96 47.27,-115.2 46.33,-114.41 45.44,-113.59 44.59,-112.75 43.78,-111.89 43.02,-111.01 42.31,-110.11 41.67,-109.2 41.08,-108.28 40.56,-107.35 40.11,-106.41 39.73,-105.47 39.43,-104.53 39.21,-103.59 39.07,-102.65 39.01,-101.72 39.04,-100.8 39.17,-99.89 39.38,-98.99 39.69,-98.11 40.09,-97.25 40.59,-96.41 41.19,-95.59 41.87,-94.8 42.65,-94.04 43.53,-93.31 44.49,-92.61 45.55,-91.94 46.68,-91.31 47.9,-90.71 49.2,-90.16 50.57,-89.65 52.01,-89.18 53.52,-88.75 55.08,-88.36 56.69,-88.03 58.35,-87.74 60.05,-87.49 61.78,-87.3 63.54,-87.15 65.32,-87.05 67.1,-87 68.9,-87 70.68,-87.05\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)->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=\"none\" stroke=\"black\" points=\"54,-297 0,-297 0,-261 54,-261 54,-297\"/>\n<text text-anchor=\"middle\" x=\"27\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">and</text>\n</g>\n<!-- and(p,or(q,not(p)))->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=\"none\" stroke=\"black\" points=\"95,-210 41,-210 41,-174 95,-174 95,-210\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">or</text>\n</g>\n<!-- and(p,or(q,not(p)))->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\"]\n", "\"q\" [shape=\"egg\", label=\"q\"]\n", "\"not(p)\" [shape=\"rect\", label=\"not\"]\n", "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\"]\n", "\"or(q,not(p))\" [shape=\"rect\", label=\"or\"]\n", " \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n", " \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n", " \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n", " \"or(q,not(p))\" -> \"q\" [label=\"1\", color=\"black\", style=\"solid\"]\n", " \"or(q,not(p))\" -> \"not(p)\" [label=\"2\", color=\"black\", style=\"solid\"]\n", "}" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3)" ] }, { "cell_type": "markdown", "id": "11b3a8ad", "metadata": {}, "source": [ "Below we will study how one can assign a truth-value to logical formulas like the one above.\n", "\n", "## Truth tables\n", "\n", "Every logical connective has a truth-table, indicating how it maps the truth of its arguments to its own truth value.\n", "For example, `and` maps inputs `true` and `false` to `false`." ] }, { "cell_type": "code", "execution_count": 22, "id": "350b9756", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [ "not(true,false).\n", "not(false,true).\n", "\n", "and(true,V,V) :- truth_value(V).\n", "and(false,_,false).\n", "\n", "or(true,_,true).\n", "or(false,V,V) :- truth_value(V).\n", "\n", "implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res).\n", "equiv(A,B,Res) :- implies(A,B,AiB), implies(B,A,BiA), and(AiB,BiA,Res).\n", "\n", "truth_value(true).\n", "truth_value(false).\n", "\n", "truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :- \n", " truth_value(A), truth_value(B),\n", " not(A,NotA), and(A,B,AandB), or(A,B,AorB),\n", " implies(A,B,AiB), equiv(A,B,AeB)." ] }, { "cell_type": "code", "execution_count": 23, "id": "54b57ff8", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/markdown": [ "A | B | NotA | AandB | AorB | AimpliesB | AequivB | \n", ":- | :- | :- | :- | :- | :- | :- | \n", "true | true | false | true | true | true | true | \n", "true | false | false | false | true | false | false | \n", "false | true | true | false | true | true | false | \n", "false | false | true | false | false | true | true | " ], "text/plain": [ "A | B | NotA | AandB | AorB | AimpliesB | AequivB | \n", ":- | :- | :- | :- | :- | :- | :- | \n", "true | true | false | true | true | true | true | \n", "true | false | false | false | true | false | false | \n", "false | true | true | false | true | true | false | \n", "false | false | true | false | false | true | true | " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))" ] }, { "cell_type": "code", "execution_count": 24, "id": "175c00d0", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [ "value(X,Interpretation,Value) :- \n", " atomic(X), % we could also use: proposition(X),\n", " member(X/Value,Interpretation).\n", "value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),\n", " and(VA,VB,Val).\n", "value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),\n", " or(VA,VB,Val).\n", "value(not(A),I,Val) :- value(A,I,VA),\n", " not(VA,Val).\n", "value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val).\n", "value(equiv(A,B),I,Val) :- \n", " value(and(implies(A,B),implies(B,A)),I,Val).\n" ] }, { "cell_type": "code", "execution_count": 25, "id": "eee17774", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mRes = false" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- value(and(p,or(q,not(p))), [p/true, q/false],Res)." ] }, { "cell_type": "code", "execution_count": 26, "id": "78473da0", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/markdown": [ "P | Q | Res | \n", ":- | :- | :- | \n", "true | true | true | \n", "true | false | false | \n", "false | true | false | \n", "false | false | false | " ], "text/plain": [ "P | Q | Res | \n", ":- | :- | :- | \n", "true | true | true | \n", "true | false | false | \n", "false | true | false | \n", "false | false | false | " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))" ] }, { "cell_type": "code", "execution_count": 27, "id": "2ee60c15", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [ "\n", "subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :- \n", " rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering\n", " functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),\n", " (value(Sub,Interpretation,true) -> C=olive ; C=sienna1)." ] }, { "cell_type": "code", "execution_count": 28, "id": "2b497dad", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Pages: 1 -->\n<svg width=\"177pt\" height=\"305pt\"\n viewBox=\"0.00 0.00 177.00 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 173,-301 173,4 -4,4\"/>\n<!-- p -->\n<g id=\"node1\" class=\"node\">\n<title>p</title>\n<polygon fill=\"olive\" stroke=\"black\" points=\"54.68,-0.05 56.46,-0.15 58.22,-0.3 59.95,-0.49 61.65,-0.74 63.31,-1.03 64.92,-1.36 66.48,-1.75 67.99,-2.18 69.43,-2.65 70.8,-3.16 72.1,-3.71 73.32,-4.31 74.45,-4.94 75.51,-5.61 76.47,-6.31 77.35,-7.04 78.13,-7.8 78.81,-8.59 79.41,-9.41 79.91,-10.25 80.31,-11.11 80.62,-11.99 80.83,-12.89 80.96,-13.8 80.99,-14.72 80.93,-15.65 80.79,-16.59 80.57,-17.53 80.27,-18.47 79.89,-19.41 79.44,-20.35 78.92,-21.28 78.33,-22.2 77.69,-23.11 76.98,-24.01 76.22,-24.89 75.41,-25.75 74.56,-26.59 73.67,-27.41 72.73,-28.2 71.76,-28.96 70.76,-29.69 69.74,-30.39 68.68,-31.06 67.61,-31.69 66.52,-32.29 65.41,-32.84 64.28,-33.35 63.14,-33.82 61.99,-34.25 60.84,-34.64 59.67,-34.97 58.5,-35.26 57.33,-35.51 56.15,-35.7 54.96,-35.85 53.78,-35.95 52.59,-36 51.41,-36 50.22,-35.95 49.04,-35.85 47.85,-35.7 46.67,-35.51 45.5,-35.26 44.33,-34.97 43.16,-34.64 42.01,-34.25 40.86,-33.82 39.72,-33.35 38.59,-32.84 37.48,-32.29 36.39,-31.69 35.32,-31.06 34.26,-30.39 33.24,-29.69 32.24,-28.96 31.27,-28.2 30.33,-27.41 29.44,-26.59 28.59,-25.75 27.78,-24.89 27.02,-24.01 26.31,-23.11 25.67,-22.2 25.08,-21.28 24.56,-20.35 24.11,-19.41 23.73,-18.47 23.43,-17.53 23.21,-16.59 23.07,-15.65 23.01,-14.72 23.04,-13.8 23.17,-12.89 23.38,-11.99 23.69,-11.11 24.09,-10.25 24.59,-9.41 25.19,-8.59 25.87,-7.8 26.65,-7.04 27.53,-6.31 28.49,-5.61 29.55,-4.94 30.68,-4.31 31.9,-3.71 33.2,-3.16 34.57,-2.65 36.01,-2.18 37.52,-1.75 39.08,-1.36 40.69,-1.03 42.35,-0.74 44.05,-0.49 45.78,-0.3 47.54,-0.15 49.32,-0.05 51.1,0 52.9,0 54.68,-0.05\"/>\n<text text-anchor=\"middle\" x=\"52\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- q -->\n<g id=\"node2\" class=\"node\">\n<title>q</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"70.68,-87.05 72.46,-87.15 74.22,-87.3 75.95,-87.49 77.65,-87.74 79.31,-88.03 80.92,-88.36 82.48,-88.75 83.99,-89.18 85.43,-89.65 86.8,-90.16 88.1,-90.71 89.32,-91.31 90.45,-91.94 91.51,-92.61 92.47,-93.31 93.35,-94.04 94.13,-94.8 94.81,-95.59 95.41,-96.41 95.91,-97.25 96.31,-98.11 96.62,-98.99 96.83,-99.89 96.96,-100.8 96.99,-101.72 96.93,-102.65 96.79,-103.59 96.57,-104.53 96.27,-105.47 95.89,-106.41 95.44,-107.35 94.92,-108.28 94.33,-109.2 93.69,-110.11 92.98,-111.01 92.22,-111.89 91.41,-112.75 90.56,-113.59 89.67,-114.41 88.73,-115.2 87.76,-115.96 86.76,-116.69 85.74,-117.39 84.68,-118.06 83.61,-118.69 82.52,-119.29 81.41,-119.84 80.28,-120.35 79.14,-120.82 77.99,-121.25 76.84,-121.64 75.67,-121.97 74.5,-122.26 73.33,-122.51 72.15,-122.7 70.96,-122.85 69.78,-122.95 68.59,-123 67.41,-123 66.22,-122.95 65.04,-122.85 63.85,-122.7 62.67,-122.51 61.5,-122.26 60.33,-121.97 59.16,-121.64 58.01,-121.25 56.86,-120.82 55.72,-120.35 54.59,-119.84 53.48,-119.29 52.39,-118.69 51.32,-118.06 50.26,-117.39 49.24,-116.69 48.24,-115.96 47.27,-115.2 46.33,-114.41 45.44,-113.59 44.59,-112.75 43.78,-111.89 43.02,-111.01 42.31,-110.11 41.67,-109.2 41.08,-108.28 40.56,-107.35 40.11,-106.41 39.73,-105.47 39.43,-104.53 39.21,-103.59 39.07,-102.65 39.01,-101.72 39.04,-100.8 39.17,-99.89 39.38,-98.99 39.69,-98.11 40.09,-97.25 40.59,-96.41 41.19,-95.59 41.87,-94.8 42.65,-94.04 43.53,-93.31 44.49,-92.61 45.55,-91.94 46.68,-91.31 47.9,-90.71 49.2,-90.16 50.57,-89.65 52.01,-89.18 53.52,-88.75 55.08,-88.36 56.69,-88.03 58.35,-87.74 60.05,-87.49 61.78,-87.3 63.54,-87.15 65.32,-87.05 67.1,-87 68.9,-87 70.68,-87.05\"/>\n<text text-anchor=\"middle\" x=\"68\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- not(p) -->\n<g id=\"node3\" class=\"node\">\n<title>not(p)</title>\n<polygon fill=\"#ff8247\" stroke=\"black\" points=\"169,-123 115,-123 115,-87 169,-87 169,-123\"/>\n<text text-anchor=\"middle\" x=\"142\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">not</text>\n</g>\n<!-- not(p)->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", "text/plain": [ "digraph {\n", "\"p\" [shape=\"egg\", label=\"p\", style=\"filled\", fillcolor=\"olive\"]\n", "\"q\" [shape=\"egg\", label=\"q\", style=\"filled\", fillcolor=\"sienna1\"]\n", "\"not(p)\" [shape=\"rect\", label=\"not\", style=\"filled\", fillcolor=\"sienna1\"]\n", "\"and(p,or(q,not(p)))\" [shape=\"rect\", label=\"and\", style=\"filled\", fillcolor=\"sienna1\"]\n", "\"or(q,not(p))\" [shape=\"rect\", label=\"or\", style=\"filled\", fillcolor=\"sienna1\"]\n", " \"not(p)\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n", " \"and(p,or(q,not(p)))\" -> \"p\" [label=\"1\", color=\"black\", style=\"solid\"]\n", " \"and(p,or(q,not(p)))\" -> \"or(q,not(p))\" [label=\"2\", color=\"black\", style=\"solid\"]\n", " \"or(q,not(p))\" -> \"q\" [label=\"1\", color=\"black\", style=\"solid\"]\n", " \"or(q,not(p))\" -> \"not(p)\" [label=\"2\", color=\"black\", style=\"solid\"]\n", "}" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3)" ] }, { "cell_type": "code", "execution_count": 29, "id": "0fd23f05", "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(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3)" ] }, { "cell_type": "code", "execution_count": 30, "id": "23775624", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mtrue" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- use_module(library(clpfd))." ] }, { "cell_type": "code", "execution_count": null, "id": "7a6e29ed", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Prolog", "language": "prolog", "name": "prolog_kernel" }, "language_info": { "codemirror_mode": "prolog", "file_extension": ".pl", "mimetype": "text/x-prolog", "name": "Prolog" } }, "nbformat": 4, "nbformat_minor": 5 }