lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

5-3-tableau.dot.svg (8311B)


      1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
      2 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
      3  "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
      4 <!-- Generated by graphviz version 2.50.0 (20211204.2007)
      5  -->
      6 <!-- Title: g Pages: 1 -->
      7 <svg width="462pt" height="524pt"
      8  viewBox="0.00 0.00 462.29 524.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
      9 <g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 520)">
     10 <title>g</title>
     11 <polygon fill="white" stroke="transparent" points="-4,4 -4,-520 458.29,-520 458.29,4 -4,4"/>
     12 <!-- a -->
     13 <g id="node1" class="node">
     14 <title>a</title>
     15 <ellipse fill="none" stroke="black" cx="237.29" cy="-483" rx="134.58" ry="18"/>
     16 <text text-anchor="middle" x="237.29" y="-479.3" font-family="Times,serif" font-size="14.00">* (¬ ◇ ¬ p ∧ ◇ ¬ q), ¬ ◇ (p ∧ ¬ q)</text>
     17 <text text-anchor="middle" x="99.25" y="-504.8" font-family="Times,serif" font-size="14.00">1</text>
     18 </g>
     19 <!-- b -->
     20 <g id="node2" class="node">
     21 <title>b</title>
     22 <ellipse fill="none" stroke="black" cx="125.29" cy="-411" rx="118.08" ry="18"/>
     23 <text text-anchor="middle" x="125.29" y="-407.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q) * ¬ ◇ ¬ p ∧ ◇ ¬ q</text>
     24 <text text-anchor="middle" x="3.5" y="-432.8" font-family="Times,serif" font-size="14.00">1</text>
     25 </g>
     26 <!-- a&#45;&#45;b -->
     27 <g id="edge1" class="edge">
     28 <title>a&#45;&#45;b</title>
     29 <path fill="none" stroke="black" d="M210.46,-465.23C192.73,-454.15 169.58,-439.68 151.9,-428.63"/>
     30 </g>
     31 <!-- la -->
     32 <g id="node3" class="node">
     33 <title>la</title>
     34 <ellipse fill="none" stroke="black" cx="350.29" cy="-411" rx="88.28" ry="18"/>
     35 <text text-anchor="middle" x="350.29" y="-407.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q) * ¬ ◇ ¬ p</text>
     36 <text text-anchor="middle" x="258.4" y="-432.8" font-family="Times,serif" font-size="14.00">1</text>
     37 </g>
     38 <!-- a&#45;&#45;la -->
     39 <g id="edge2" class="edge">
     40 <title>a&#45;&#45;la</title>
     41 <path fill="none" stroke="black" d="M264.36,-465.23C282.38,-454.07 305.94,-439.47 323.83,-428.39"/>
     42 </g>
     43 <!-- ra -->
     44 <g id="node9" class="node">
     45 <title>ra</title>
     46 <ellipse fill="none" stroke="black" cx="125.29" cy="-339" rx="80.69" ry="18"/>
     47 <text text-anchor="middle" x="125.29" y="-335.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q) * ◇ ¬ q</text>
     48 <text text-anchor="middle" x="41.2" y="-360.8" font-family="Times,serif" font-size="14.00">1</text>
     49 </g>
     50 <!-- b&#45;&#45;ra -->
     51 <g id="edge8" class="edge">
     52 <title>b&#45;&#45;ra</title>
     53 <path fill="none" stroke="black" d="M125.29,-392.7C125.29,-381.85 125.29,-367.92 125.29,-357.1"/>
     54 </g>
     55 <!-- lb -->
     56 <g id="node4" class="node">
     57 <title>lb</title>
     58 <ellipse fill="none" stroke="black" cx="350.29" cy="-339" rx="83.39" ry="18"/>
     59 <text text-anchor="middle" x="350.29" y="-335.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q), ◇ ¬ p *</text>
     60 <text text-anchor="middle" x="263.6" y="-360.8" font-family="Times,serif" font-size="14.00">1</text>
     61 </g>
     62 <!-- la&#45;&#45;lb -->
     63 <g id="edge3" class="edge">
     64 <title>la&#45;&#45;lb</title>
     65 <path fill="none" stroke="black" d="M350.29,-392.7C350.29,-381.85 350.29,-367.92 350.29,-357.1"/>
     66 </g>
     67 <!-- lla -->
     68 <g id="node5" class="node">
     69 <title>lla</title>
     70 <ellipse fill="none" stroke="black" cx="298.29" cy="-261.5" rx="44.39" ry="18"/>
     71 <text text-anchor="middle" x="298.29" y="-257.8" font-family="Times,serif" font-size="14.00">p ∧ ¬ q *</text>
     72 <text text-anchor="middle" x="250.59" y="-283.3" font-family="Times,serif" font-size="14.00">2</text>
     73 </g>
     74 <!-- lb&#45;&#45;lla -->
     75 <g id="edge4" class="edge">
     76 <title>lb&#45;&#45;lla</title>
     77 <path fill="none" stroke="black" stroke-dasharray="5,2" d="M338.49,-320.87C329.86,-308.34 318.22,-291.44 309.69,-279.05"/>
     78 </g>
     79 <!-- lra -->
     80 <g id="node8" class="node">
     81 <title>lra</title>
     82 <polygon fill="none" stroke="black" points="360.29,-238.5 360.29,-284.5 454.29,-284.5 454.29,-238.5 360.29,-238.5"/>
     83 <text text-anchor="middle" x="407.29" y="-269.3" font-family="Times,serif" font-size="14.00">¬ p *</text>
     84 <polyline fill="none" stroke="black" points="360.29,-261.5 454.29,-261.5 "/>
     85 <text text-anchor="middle" x="407.29" y="-246.3" font-family="Times,serif" font-size="14.00">does not close</text>
     86 <text text-anchor="middle" x="356.79" y="-288.8" font-family="Times,serif" font-size="14.00">3</text>
     87 </g>
     88 <!-- lb&#45;&#45;lra -->
     89 <g id="edge7" class="edge">
     90 <title>lb&#45;&#45;lra</title>
     91 <path fill="none" stroke="black" stroke-dasharray="5,2" d="M363.22,-320.87C371.3,-310.17 381.79,-296.27 390.51,-284.73"/>
     92 </g>
     93 <!-- llb -->
     94 <g id="node6" class="node">
     95 <title>llb</title>
     96 <ellipse fill="none" stroke="black" cx="298.29" cy="-184" rx="38.99" ry="18"/>
     97 <text text-anchor="middle" x="298.29" y="-180.3" font-family="Times,serif" font-size="14.00">p, ¬ q *</text>
     98 <text text-anchor="middle" x="255.79" y="-205.8" font-family="Times,serif" font-size="14.00">2</text>
     99 </g>
    100 <!-- lla&#45;&#45;llb -->
    101 <g id="edge5" class="edge">
    102 <title>lla&#45;&#45;llb</title>
    103 <path fill="none" stroke="black" d="M298.29,-243.37C298.29,-231.01 298.29,-214.4 298.29,-202.06"/>
    104 </g>
    105 <!-- llc -->
    106 <g id="node7" class="node">
    107 <title>llc</title>
    108 <polygon fill="none" stroke="black" points="251.29,-83.5 251.29,-129.5 345.29,-129.5 345.29,-83.5 251.29,-83.5"/>
    109 <text text-anchor="middle" x="298.29" y="-114.3" font-family="Times,serif" font-size="14.00">p * q</text>
    110 <polyline fill="none" stroke="black" points="251.29,-106.5 345.29,-106.5 "/>
    111 <text text-anchor="middle" x="298.29" y="-91.3" font-family="Times,serif" font-size="14.00">does not close</text>
    112 <text text-anchor="middle" x="247.79" y="-133.8" font-family="Times,serif" font-size="14.00">2</text>
    113 </g>
    114 <!-- llb&#45;&#45;llc -->
    115 <g id="edge6" class="edge">
    116 <title>llb&#45;&#45;llc</title>
    117 <path fill="none" stroke="black" d="M298.29,-165.87C298.29,-155.17 298.29,-141.27 298.29,-129.73"/>
    118 </g>
    119 <!-- rb -->
    120 <g id="node10" class="node">
    121 <title>rb</title>
    122 <ellipse fill="none" stroke="black" cx="125.29" cy="-261.5" rx="59.29" ry="18"/>
    123 <text text-anchor="middle" x="125.29" y="-257.8" font-family="Times,serif" font-size="14.00">p ∧ ¬ q * ¬ q</text>
    124 <text text-anchor="middle" x="62.64" y="-283.3" font-family="Times,serif" font-size="14.00">4</text>
    125 </g>
    126 <!-- ra&#45;&#45;rb -->
    127 <g id="edge9" class="edge">
    128 <title>ra&#45;&#45;rb</title>
    129 <path fill="none" stroke="black" stroke-dasharray="5,2" d="M125.29,-320.87C125.29,-308.51 125.29,-291.9 125.29,-279.56"/>
    130 </g>
    131 <!-- rc -->
    132 <g id="node11" class="node">
    133 <title>rc</title>
    134 <ellipse fill="none" stroke="black" cx="125.29" cy="-184" rx="53.89" ry="18"/>
    135 <text text-anchor="middle" x="125.29" y="-180.3" font-family="Times,serif" font-size="14.00">p ∧ ¬ q, q *</text>
    136 <text text-anchor="middle" x="67.84" y="-205.8" font-family="Times,serif" font-size="14.00">4</text>
    137 </g>
    138 <!-- rb&#45;&#45;rc -->
    139 <g id="edge10" class="edge">
    140 <title>rb&#45;&#45;rc</title>
    141 <path fill="none" stroke="black" d="M125.29,-243.37C125.29,-231.01 125.29,-214.4 125.29,-202.06"/>
    142 </g>
    143 <!-- rd -->
    144 <g id="node12" class="node">
    145 <title>rd</title>
    146 <ellipse fill="none" stroke="black" cx="125.29" cy="-106.5" rx="48.19" ry="18"/>
    147 <text text-anchor="middle" x="125.29" y="-102.8" font-family="Times,serif" font-size="14.00">p, ¬ q, q *</text>
    148 <text text-anchor="middle" x="73.69" y="-128.3" font-family="Times,serif" font-size="14.00">4</text>
    149 </g>
    150 <!-- rc&#45;&#45;rd -->
    151 <g id="edge11" class="edge">
    152 <title>rc&#45;&#45;rd</title>
    153 <path fill="none" stroke="black" d="M125.29,-165.87C125.29,-153.51 125.29,-136.9 125.29,-124.56"/>
    154 </g>
    155 <!-- re -->
    156 <g id="node13" class="node">
    157 <title>re</title>
    158 <polygon fill="none" stroke="black" points="95.79,-0.5 95.79,-46.5 154.79,-46.5 154.79,-0.5 95.79,-0.5"/>
    159 <text text-anchor="middle" x="125.29" y="-31.3" font-family="Times,serif" font-size="14.00">p, q * q</text>
    160 <polyline fill="none" stroke="black" points="95.79,-23.5 154.79,-23.5 "/>
    161 <text text-anchor="middle" x="125.29" y="-8.3" font-family="Times,serif" font-size="14.00">closes</text>
    162 <text text-anchor="middle" x="92.29" y="-50.8" font-family="Times,serif" font-size="14.00">4</text>
    163 </g>
    164 <!-- rd&#45;&#45;re -->
    165 <g id="edge12" class="edge">
    166 <title>rd&#45;&#45;re</title>
    167 <path fill="none" stroke="black" d="M125.29,-88.32C125.29,-76.15 125.29,-59.73 125.29,-46.59"/>
    168 </g>
    169 </g>
    170 </svg>