commit c3fdf7b6be10240d960e88d991606a1cab3755b1 parent 804420fcae444471dade15b49b6d1847923b6088 Author: Alex Balgavy <alex@balgavy.eu> Date: Tue, 8 Mar 2022 21:09:15 +0100 Update advanced logic notes Diffstat:
16 files changed, 738 insertions(+), 2 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md @@ -12,6 +12,8 @@ title = 'Advanced Logic' 8. [Exercise 3](exercise-3/) 9. [Lecture 7](lecture-7/) 10. [Homework 1](homework-1/) +11. [Lecture 8](lecture-8/) +12. [Lecture 9](lecture-9/) I drew the graphs on these pages with [Graphviz](https://graphviz.org/), I used [vim-literate-markdown](https://github.com/thezeroalpha/vim-literate-markdown)'s tangling functionality to quickly extract graph code to separate files. You can install Graphviz and run e.g. `dot < graph.dot -Tsvg > graph.svg` (also accepts input files as parameters). diff --git a/content/advanced-logic-notes/lecture-1/index.md b/content/advanced-logic-notes/lecture-1/index.md @@ -31,9 +31,9 @@ If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ If v ⊨ φ for all valuations of v, then ⊨ φ (φ is a tautology) -Soundness: ⊢ implies ⊨, proved by induction on length of proof +Soundness: ⊢ implies ⊨ -- what we can derive is true. proved by induction on length of proof -Completeness: ⊨ implies ⊢, can be proven using consistency +Completeness: ⊨ implies ⊢ -- we can derive what is true. can be proven using consistency # Basic modal logic E.g. "whatever is necessary is possible" == □φ → ◇φ diff --git a/content/advanced-logic-notes/lecture-4/index.md b/content/advanced-logic-notes/lecture-4/index.md @@ -32,6 +32,92 @@ Therefore, the top states of both models are _bisimilar_. Since all of the states in the models are bisimilar, _the two models are bisimilar_. The dotted lines connect the pairs that make up the _bisimulation_. +### Example: finding bisimulations + +Take two example models: + +<table> +<thead> +<th>A</th> <th>B</th> +</thead> + +<tbody> +<tr> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-a.dot --> +```dot +digraph g { +1 -> 2 +2 -> 3 +3 -> 4 +3 -> 5 +1 [xlabel="p"] +2 [xlabel="q"] +3 [xlabel="q"] +4 [xlabel="q"] +5 [xlabel="q"] +} +``` + +</details> +</td> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-b.dot --> +```dot +digraph g { +a -> b +a -> c +c -> d +b -> d +d -> e +a [xlabel="p"] +b [xlabel="q"] +c [xlabel="q"] +d [xlabel="q"] +e [xlabel="q"] +} +``` + +</details> +</td> + +</tr> +</table> + +The claim is that states (A,1) and (B,a) are bisimilar. +How do you prove or refute the claim? + +Well, we need to find a bisimulation with the pair (1, a). +1. Start with pair (1, a) +2. In A, move from 1 to 2. Have to mimic the move in B, can do so by moving from a to b or from a to c. + Yields the pairs (2, b) and (2, c). +3. In A, move from 2 to 3. Have to mimic the move in B, can move from both b and c to d. + Yields the pair (3, d). +4. In A, two options: + - move from 3 to 4. Have to mimic the move in B, can move from d to e. + Yields the pair (4, e). + - move from 3 to 5. Have to mimic the move in B, can move from d to e. + Yields the pair (5, e). + +Since for any move in the first model, we can mimic it in the second model, we have a bisimulation. +The bisimulation contains exactly the pairs we just listed. +So there is a bisimulation Z = {(1, a), (2, b), (2, c), (3, d), (4, e), (5, e)}. +Since (1, a) ∈ Z, we can say that states (A, 1) and (B, a) are bisimilar. + ## Transforming and constructing models Disjoint union of models: combine models by union of states, relations, and valuations. A state in one of the models is modally equivalent with the state in the union. diff --git a/content/advanced-logic-notes/lecture-4/model-a.dot b/content/advanced-logic-notes/lecture-4/model-a.dot @@ -0,0 +1,12 @@ +digraph g { +1 -> 2 +2 -> 3 +3 -> 4 +3 -> 5 +1 [xlabel="p"] +2 [xlabel="q"] +3 [xlabel="q"] +4 [xlabel="q"] +5 [xlabel="q"] +} + diff --git a/content/advanced-logic-notes/lecture-4/model-a.dot.svg b/content/advanced-logic-notes/lecture-4/model-a.dot.svg @@ -0,0 +1,72 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" + "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<!-- Generated by graphviz version 2.50.0 (20211204.2007) + --> +<!-- Title: g Pages: 1 --> +<svg width="141pt" height="275pt" + viewBox="0.00 0.00 141.00 275.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"> +<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 271)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-271 137,-271 137,4 -4,4"/> +<!-- 1 --> +<g id="node1" class="node"> +<title>1</title> +<ellipse fill="none" stroke="black" cx="70" cy="-234" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-230.3" font-family="Times,serif" font-size="14.00">1</text> +<text text-anchor="middle" x="39.5" y="-255.8" font-family="Times,serif" font-size="14.00">p</text> +</g> +<!-- 2 --> +<g id="node2" class="node"> +<title>2</title> +<ellipse fill="none" stroke="black" cx="70" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-158.3" font-family="Times,serif" font-size="14.00">2</text> +<text text-anchor="middle" x="39.5" y="-183.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- 1->2 --> +<g id="edge1" class="edge"> +<title>1->2</title> +<path fill="none" stroke="black" d="M70,-215.7C70,-207.98 70,-198.71 70,-190.11"/> +<polygon fill="black" stroke="black" points="73.5,-190.1 70,-180.1 66.5,-190.1 73.5,-190.1"/> +</g> +<!-- 3 --> +<g id="node3" class="node"> +<title>3</title> +<ellipse fill="none" stroke="black" cx="70" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-86.3" font-family="Times,serif" font-size="14.00">3</text> +<text text-anchor="middle" x="39.5" y="-111.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- 2->3 --> +<g id="edge2" class="edge"> +<title>2->3</title> +<path fill="none" stroke="black" d="M70,-143.7C70,-135.98 70,-126.71 70,-118.11"/> +<polygon fill="black" stroke="black" points="73.5,-118.1 70,-108.1 66.5,-118.1 73.5,-118.1"/> +</g> +<!-- 4 --> +<g id="node4" class="node"> +<title>4</title> +<ellipse fill="none" stroke="black" cx="34" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="34" y="-14.3" font-family="Times,serif" font-size="14.00">4</text> +<text text-anchor="middle" x="3.5" y="-39.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- 3->4 --> +<g id="edge3" class="edge"> +<title>3->4</title> +<path fill="none" stroke="black" d="M61.65,-72.76C57.29,-64.28 51.85,-53.71 46.96,-44.2"/> +<polygon fill="black" stroke="black" points="49.99,-42.44 42.3,-35.15 43.77,-45.64 49.99,-42.44"/> +</g> +<!-- 5 --> +<g id="node5" class="node"> +<title>5</title> +<ellipse fill="none" stroke="black" cx="106" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="106" y="-14.3" font-family="Times,serif" font-size="14.00">5</text> +<text text-anchor="middle" x="75.5" y="-39.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- 3->5 --> +<g id="edge4" class="edge"> +<title>3->5</title> +<path fill="none" stroke="black" d="M78.35,-72.76C82.71,-64.28 88.15,-53.71 93.04,-44.2"/> +<polygon fill="black" stroke="black" points="96.23,-45.64 97.7,-35.15 90.01,-42.44 96.23,-45.64"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-4/model-b.dot b/content/advanced-logic-notes/lecture-4/model-b.dot @@ -0,0 +1,13 @@ +digraph g { +a -> b +a -> c +c -> d +b -> d +d -> e +a [xlabel="p"] +b [xlabel="q"] +c [xlabel="q"] +d [xlabel="q"] +e [xlabel="q"] +} + diff --git a/content/advanced-logic-notes/lecture-4/model-b.dot.svg b/content/advanced-logic-notes/lecture-4/model-b.dot.svg @@ -0,0 +1,78 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" + "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<!-- Generated by graphviz version 2.50.0 (20211204.2007) + --> +<!-- Title: g Pages: 1 --> +<svg width="141pt" height="275pt" + viewBox="0.00 0.00 141.00 275.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"> +<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 271)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-271 137,-271 137,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="70" cy="-234" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-230.3" font-family="Times,serif" font-size="14.00">a</text> +<text text-anchor="middle" x="39.5" y="-255.8" font-family="Times,serif" font-size="14.00">p</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="34" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="34" y="-158.3" font-family="Times,serif" font-size="14.00">b</text> +<text text-anchor="middle" x="3.5" y="-183.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- a->b --> +<g id="edge1" class="edge"> +<title>a->b</title> +<path fill="none" stroke="black" d="M61.65,-216.76C57.29,-208.28 51.85,-197.71 46.96,-188.2"/> +<polygon fill="black" stroke="black" points="49.99,-186.44 42.3,-179.15 43.77,-189.64 49.99,-186.44"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</title> +<ellipse fill="none" stroke="black" cx="106" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="106" y="-158.3" font-family="Times,serif" font-size="14.00">c</text> +<text text-anchor="middle" x="75.5" y="-183.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- a->c --> +<g id="edge2" class="edge"> +<title>a->c</title> +<path fill="none" stroke="black" d="M78.35,-216.76C82.71,-208.28 88.15,-197.71 93.04,-188.2"/> +<polygon fill="black" stroke="black" points="96.23,-189.64 97.7,-179.15 90.01,-186.44 96.23,-189.64"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</title> +<ellipse fill="none" stroke="black" cx="70" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-86.3" font-family="Times,serif" font-size="14.00">d</text> +<text text-anchor="middle" x="39.5" y="-111.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- b->d --> +<g id="edge4" class="edge"> +<title>b->d</title> +<path fill="none" stroke="black" d="M42.35,-144.76C46.71,-136.28 52.15,-125.71 57.04,-116.2"/> +<polygon fill="black" stroke="black" points="60.23,-117.64 61.7,-107.15 54.01,-114.44 60.23,-117.64"/> +</g> +<!-- c->d --> +<g id="edge3" class="edge"> +<title>c->d</title> +<path fill="none" stroke="black" d="M97.65,-144.76C93.29,-136.28 87.85,-125.71 82.96,-116.2"/> +<polygon fill="black" stroke="black" points="85.99,-114.44 78.3,-107.15 79.77,-117.64 85.99,-114.44"/> +</g> +<!-- e --> +<g id="node5" class="node"> +<title>e</title> +<ellipse fill="none" stroke="black" cx="70" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-14.3" font-family="Times,serif" font-size="14.00">e</text> +<text text-anchor="middle" x="39.5" y="-39.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- d->e --> +<g id="edge5" class="edge"> +<title>d->e</title> +<path fill="none" stroke="black" d="M70,-71.7C70,-63.98 70,-54.71 70,-46.11"/> +<polygon fill="black" stroke="black" points="73.5,-46.1 70,-36.1 66.5,-46.1 73.5,-46.1"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-8/Screenshot 2022-03-05 at 12.06.06.png b/content/advanced-logic-notes/lecture-8/Screenshot 2022-03-05 at 12.06.06.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-8/admissible-rule.png b/content/advanced-logic-notes/lecture-8/admissible-rule.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-8/index.md b/content/advanced-logic-notes/lecture-8/index.md @@ -0,0 +1,190 @@ ++++ +title = 'Lecture 8' ++++ +# Lecture 8 +## Modal tautologies + + + +## Proof systems +Hilbert systems: +- proof is sequence of numbered formulas +- every formula is: an axiom, or result of applying a derivation rule + +Sufficient to have 2 axioms and a rule: +- K: φ → ψ → φ +- S: (φ → ψ → θ) → (φ → ψ) → (φ → θ) +- modus ponens: if φ and (φ → ψ), then ψ + +Rules will be given, don't need to be memorized. + +Admissible rule: + + + +Proof system K is sound and complete with respect to all frames, ⊢K φ iff ⊨ φ. + +<!-- TODO: add this to anki --> +Need to memorize soundness and completeness results +- K sound and complete for all frames +- T sound and complete for all _reflexive_ frames + - T: K with □ p → p +- S4 sound and complete for all _reflexive-transitive_ frames + - S4: T with □ p → □ □ p +- S5 sound and complete for for frames with R an equivalence relation + - S5: S4 with ¬ □ p → □ ¬ □ p + +## Example of derivation +Give derivation in K of ◇ φ ∧ □ (φ → ψ) → ◇ ψ. +Same as example in book <abbr title='Modal Logic for Open Minds (Benthem)'>MLOM</abbr> page 52. + +First, work backwards from the goal towards an axiom or tautology: + +``` +◇ φ ∧ □ (φ → ψ) → ◇ ψ ≡ □ (φ → ψ) → (◇ φ → ◇ ψ) [you can rewrite a conjunction as an implication] + ≡ □ (φ → ψ) → (¬ □ ¬ φ → ¬ □ ¬ ψ) [rewrite diamond to ¬ □ ¬] + ≡ □ (φ → ψ) → (□ ¬ ψ → □ ¬ φ) [rewrite contrapositive (¬ a → ¬ b) to (b → a)] + ≡ □ (φ → ψ) → □ (¬ ψ → ¬ φ) [box distribution over implication] + ≡ □ (φ → ψ) → □ (φ → ψ) [again contrapositive] + ≡ (φ → ψ) → (φ → ψ) [because if derivable (a → b), then derivable (□ a → □ b)] +``` + +We arrive at a tautology. + +Then you write it out in a Hilbert-style proof, starting with the tautology/axiom. +PROP means rewriting in propositional logic. + +1. (φ → ψ) → (¬ ψ → ¬ φ). PROP. +2. □ (φ → ψ) → □ (¬ ψ → ¬ φ). DISTR, 1. +3. □ (p → q) → □ p → □ q. modal distribution (i.e., this is an axiom in K that we use) +4. □ (¬ ψ → ¬ φ) → □ ¬ ψ → □ ¬ φ. substitution, 3 (i.e., substitute stuff in the axiom). +5. □ (φ → ψ) → □ ¬ ψ → □ ¬ φ. PROP, 2, 4. +6. □ (φ → ψ) → ¬ ◇ ψ → ¬ ◇ φ. definition of ◇, □. +7. □ (φ → ψ) → ◇ φ → ◇ ψ. PROP, 6. +8. ◇ φ ∧ □ (φ → ψ) → ◇ ψ. PROP, 7. + +<details> +<summary>Why you can rewrite a conjunction as an implication</summary> + +You can safely rewrite a conjunction to an implication: (a ∧ b → c) ≡ a → (b → c). +Remember that implication is right-associative! + +If you don't trust me, I didn't trust myself either so I made a truth table: + +<table> +<thead> +<tr> +<th>a</th> +<th>b</th> +<th>c</th> +<th>b → c</th> +<th>a ∧ b</th> +<th>a → c</th> +<th>a ∧ b → c</th> +<th>b → (a → c)</th> +<th>a → (b → c)</th> +</tr> +</thead> +<tbody> +<tr> +<td>0</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>0</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>0</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>1</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>1</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>0</td> +<td>0</td> +</tr> + +<tr> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> +</tbody> +</table> + +You see that the right three columns all have the same values, so semantically the formulas are the same. + +</details> + diff --git a/content/advanced-logic-notes/lecture-8/modal-tautologies.png b/content/advanced-logic-notes/lecture-8/modal-tautologies.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-9/index.md b/content/advanced-logic-notes/lecture-9/index.md @@ -0,0 +1,122 @@ ++++ +title = 'Lecture 9' ++++ +# Lecture 9 +## Temporal logic using temporal frames +Linear time logic: events along a single computation path. 'at some point we will have p' + +Branching time logic: quantify over possible paths. 'there is a path where eventually p' + +A frame F = (T, <) is a temporal frame if both: +- < is irreflexive: not t < t for all t +- < is transitive: if t < u and u < v then t < v + +Right-linearity: +- "all future points are related" +- definition: ∀ x,y,z: (x < y) ∧ (x < z) → (y < z) ∨ (y = z) ∨ (z < y) +- is modally definable + +Right-branching: +- "right-branching is _not_ right-linear, so some point has two unrelated points in the future" +- definition: there exist x,y,z such that x < y and x < z but ¬ (y < z) ∧ y ≠ z ∧ ¬ (z < y) +- is _not_ modally definable + +Discrete: +- "every point with a successor has an immediate successor +- definition: (x < y ) → ∃ z : x < z ∧ ¬ ∃ u: ( x < u) ∧ (u < z) +- is modally definable in basic temporal logic + +Dense: +- "between any two points is a third one" +- definition: x < z → ∃ y (x < y ∧ y < z) +- is modally definable + +Operator next: +- symbol ⊗ +- M,t ⊨ ⊗ φ iff ∃ v : t < v ∧ (¬ ∃ u : t < u < v) ∧ M,v ⊨ φ + - e.g. x ⊨ ⊗p: there a future we can reach only in 1 step from x where p holds + - you can go directly from centraal to Utrecht, but Amstelstation is still there +- next not definable in basic modal logic + +Operator until: +- symbol U +- M,t ⊨ φ U ψ iff ∃ v : t < v ∧ M,v ⊨ ψ ∧ ∀ u : t < u < v → M,u ⊨ φ + - if we have a future where ψ holds, then φ holds in all points between now and that future +- not definable in basic modal logic + +Examples of until: + +<table> +<tr> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) until-1.dot --> +```dot +digraph g { +rankdir=BT +a -> b +a -> c +c -> d +b -> d +c -> e +c [xlabel="p"] +d [xlabel="q"] +e [xlabel="q"] +} +``` +</details> + +</td> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) until-2.dot --> +```dot +digraph g { +rankdir=BT +a -> b +a -> c +c -> d +b -> d +d [xlabel="q"] +c [xlabel="p"] +} +``` + +</details> +</td> +</tr> + +<tr> +<td> +a ⊨ p U q. e.g. state e, we have q, and in any paths we have to go through states that have p. +</td> + +<td> +a ⊭ p U q. because we do not have p in state b. +</td> +</tr> +</table> + +In a temporal frame: +- ◇ p is equivalent to T U p +- ⊗ p i equivalent to ⊥ U p + +<!-- +TODO: Things to look at: +- until not definable in basic modal logic in temporal frames +- until not definable in temporal modal logic in temporal frames +- next not definable in basic modal logic in temporal frames +- define discrete in temporal logic +- use next to define discrete in temporal logic +- define right-linearity in temporal logic +--> diff --git a/content/advanced-logic-notes/lecture-9/until-1.dot b/content/advanced-logic-notes/lecture-9/until-1.dot @@ -0,0 +1,12 @@ +digraph g { +rankdir=BT +a -> b +a -> c +c -> d +b -> d +c -> e +c [xlabel="p"] +d [xlabel="q"] +e [xlabel="q"] +} + diff --git a/content/advanced-logic-notes/lecture-9/until-1.dot.svg b/content/advanced-logic-notes/lecture-9/until-1.dot.svg @@ -0,0 +1,76 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" + "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<!-- Generated by graphviz version 2.50.0 (20211204.2007) + --> +<!-- Title: g Pages: 1 --> +<svg width="141pt" height="188pt" + viewBox="0.00 0.00 141.00 188.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"> +<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 184)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-184 137,-184 137,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="70" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="70" y="-14.3" font-family="Times,serif" font-size="14.00">a</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="34" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="34" y="-86.3" font-family="Times,serif" font-size="14.00">b</text> +</g> +<!-- a->b --> +<g id="edge1" class="edge"> +<title>a->b</title> +<path fill="none" stroke="black" d="M61.65,-35.24C57.29,-43.72 51.85,-54.29 46.96,-63.8"/> +<polygon fill="black" stroke="black" points="43.77,-62.36 42.3,-72.85 49.99,-65.56 43.77,-62.36"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</title> +<ellipse fill="none" stroke="black" cx="106" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="106" y="-86.3" font-family="Times,serif" font-size="14.00">c</text> +<text text-anchor="middle" x="75.5" y="-60.8" font-family="Times,serif" font-size="14.00">p</text> +</g> +<!-- a->c --> +<g id="edge2" class="edge"> +<title>a->c</title> +<path fill="none" stroke="black" d="M78.35,-35.24C82.71,-43.72 88.15,-54.29 93.04,-63.8"/> +<polygon fill="black" stroke="black" points="90.01,-65.56 97.7,-72.85 96.23,-62.36 90.01,-65.56"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</title> +<ellipse fill="none" stroke="black" cx="34" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="34" y="-158.3" font-family="Times,serif" font-size="14.00">d</text> +<text text-anchor="middle" x="3.5" y="-132.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- b->d --> +<g id="edge4" class="edge"> +<title>b->d</title> +<path fill="none" stroke="black" d="M34,-108.3C34,-116.02 34,-125.29 34,-133.89"/> +<polygon fill="black" stroke="black" points="30.5,-133.9 34,-143.9 37.5,-133.9 30.5,-133.9"/> +</g> +<!-- c->d --> +<g id="edge3" class="edge"> +<title>c->d</title> +<path fill="none" stroke="black" d="M91.43,-105.17C81.25,-115.06 67.48,-128.45 55.97,-139.64"/> +<polygon fill="black" stroke="black" points="53.53,-137.13 48.8,-146.62 58.41,-142.15 53.53,-137.13"/> +</g> +<!-- e --> +<g id="node5" class="node"> +<title>e</title> +<ellipse fill="none" stroke="black" cx="106" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="106" y="-158.3" font-family="Times,serif" font-size="14.00">e</text> +<text text-anchor="middle" x="75.5" y="-132.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- c->e --> +<g id="edge5" class="edge"> +<title>c->e</title> +<path fill="none" stroke="black" d="M106,-108.3C106,-116.02 106,-125.29 106,-133.89"/> +<polygon fill="black" stroke="black" points="102.5,-133.9 106,-143.9 109.5,-133.9 102.5,-133.9"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-9/until-2.dot b/content/advanced-logic-notes/lecture-9/until-2.dot @@ -0,0 +1,10 @@ +digraph g { +rankdir=BT +a -> b +a -> c +c -> d +b -> d +d [xlabel="q"] +c [xlabel="p"] +} + diff --git a/content/advanced-logic-notes/lecture-9/until-2.dot.svg b/content/advanced-logic-notes/lecture-9/until-2.dot.svg @@ -0,0 +1,63 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" + "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<!-- Generated by graphviz version 2.50.0 (20211204.2007) + --> +<!-- Title: g Pages: 1 --> +<svg width="134pt" height="188pt" + viewBox="0.00 0.00 134.00 188.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"> +<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 184)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-184 130,-184 130,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="63" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="63" y="-14.3" font-family="Times,serif" font-size="14.00">a</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="27" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="27" y="-86.3" font-family="Times,serif" font-size="14.00">b</text> +</g> +<!-- a->b --> +<g id="edge1" class="edge"> +<title>a->b</title> +<path fill="none" stroke="black" d="M54.65,-35.24C50.29,-43.72 44.85,-54.29 39.96,-63.8"/> +<polygon fill="black" stroke="black" points="36.77,-62.36 35.3,-72.85 42.99,-65.56 36.77,-62.36"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</title> +<ellipse fill="none" stroke="black" cx="99" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="99" y="-86.3" font-family="Times,serif" font-size="14.00">c</text> +<text text-anchor="middle" x="68.5" y="-60.8" font-family="Times,serif" font-size="14.00">p</text> +</g> +<!-- a->c --> +<g id="edge2" class="edge"> +<title>a->c</title> +<path fill="none" stroke="black" d="M71.35,-35.24C75.71,-43.72 81.15,-54.29 86.04,-63.8"/> +<polygon fill="black" stroke="black" points="83.01,-65.56 90.7,-72.85 89.23,-62.36 83.01,-65.56"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</title> +<ellipse fill="none" stroke="black" cx="63" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="63" y="-158.3" font-family="Times,serif" font-size="14.00">d</text> +<text text-anchor="middle" x="32.5" y="-132.8" font-family="Times,serif" font-size="14.00">q</text> +</g> +<!-- b->d --> +<g id="edge4" class="edge"> +<title>b->d</title> +<path fill="none" stroke="black" d="M35.35,-107.24C39.71,-115.72 45.15,-126.29 50.04,-135.8"/> +<polygon fill="black" stroke="black" points="47.01,-137.56 54.7,-144.85 53.23,-134.36 47.01,-137.56"/> +</g> +<!-- c->d --> +<g id="edge3" class="edge"> +<title>c->d</title> +<path fill="none" stroke="black" d="M90.65,-107.24C86.29,-115.72 80.85,-126.29 75.96,-135.8"/> +<polygon fill="black" stroke="black" points="72.77,-134.36 71.3,-144.85 78.99,-137.56 72.77,-134.36"/> +</g> +</g> +</svg>
