commit 13befac35ead3dada88cb30e1d38f24b7baa3446
parent c3fdf7b6be10240d960e88d991606a1cab3755b1
Author: Alex Balgavy <alex@balgavy.eu>
Date: Thu, 10 Mar 2022 10:38:49 +0100
Update advanced logic notes
Diffstat:
6 files changed, 120 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -14,6 +14,7 @@ title = 'Advanced Logic'
10. [Homework 1](homework-1/)
11. [Lecture 8](lecture-8/)
12. [Lecture 9](lecture-9/)
+13. [Lecture 10](lecture-10/)
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-10/example-multimodal-logic-formula.dot b/content/advanced-logic-notes/lecture-10/example-multimodal-logic-formula.dot
@@ -0,0 +1,6 @@
+digraph g {
+rankdir=LR
+1 -> 2 [label="a"]
+2 -> 3 [label="b"]
+}
+
diff --git a/content/advanced-logic-notes/lecture-10/example-multimodal-logic-formula.dot.svg b/content/advanced-logic-notes/lecture-10/example-multimodal-logic-formula.dot.svg
@@ -0,0 +1,45 @@
+<?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="256pt" height="44pt"
+ viewBox="0.00 0.00 256.00 44.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 40)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-40 252,-40 252,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-14.3" font-family="Times,serif" font-size="14.00">1</text>
+</g>
+<!-- 2 -->
+<g id="node2" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="124" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="124" y="-14.3" font-family="Times,serif" font-size="14.00">2</text>
+</g>
+<!-- 1->2 -->
+<g id="edge1" class="edge">
+<title>1->2</title>
+<path fill="none" stroke="black" d="M54.21,-18C64.28,-18 75.96,-18 86.81,-18"/>
+<polygon fill="black" stroke="black" points="86.87,-21.5 96.87,-18 86.87,-14.5 86.87,-21.5"/>
+<text text-anchor="middle" x="75.5" y="-21.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- 3 -->
+<g id="node3" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="221" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="221" y="-14.3" font-family="Times,serif" font-size="14.00">3</text>
+</g>
+<!-- 2->3 -->
+<g id="edge2" class="edge">
+<title>2->3</title>
+<path fill="none" stroke="black" d="M151.21,-18C161.28,-18 172.96,-18 183.81,-18"/>
+<polygon fill="black" stroke="black" points="183.87,-21.5 193.87,-18 183.87,-14.5 183.87,-21.5"/>
+<text text-anchor="middle" x="172.5" y="-21.8" font-family="Times,serif" font-size="14.00">b</text>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/lecture-10/index.md b/content/advanced-logic-notes/lecture-10/index.md
@@ -0,0 +1,64 @@
++++
+title = 'Lecture 10'
++++
+# Lecture 10
+## Multi-modal logic
+Assume set of labels I (which in a diagram are on the arrows).
+For every label i there is modality 〈i〉 so the formulas of multi-modal logic are, given I, defined for i in ∈ I.
+
+I-frame is pair (W, {Rᵢ | i ∈ I}).
+Rᵢ ⊆ W × W for every i ⊆ I.
+
+I-model is triple (W, {Rᵢ | i ⊆ I}, V).
+
+### Truth and validity
+For M an I-model, M,w ⊨ φ is defined by induction on the definition of formulas.
+
+Clauses:
+- M,w ⊨ 〈a〉φ iff M,v ⊨ φ for some v with Rₐwv
+- M,w ⊨ [a]φ iff M,v ⊨ φ for all v with Rₐwv
+
+### Example
+Use index set I = {a, b, c}.
+Give model with a world where the formula 〈a〉(〈b〉[a] p ∧ [c] ¬ 〈a〉p) is true.
+
+
+
+<details>
+<summary>Graphviz code</summary>
+
+<!-- :Tangle(dot) example-multimodal-logic-formula.dot -->
+```dot
+digraph g {
+rankdir=LR
+1 -> 2 [label="a"]
+2 -> 3 [label="b"]
+}
+```
+
+</details>
+
+
+For a bisimulation, when you do a step between states, they have to be with the same label (so the mimic step must have the same label).
+
+### Geach axiom
+◇ □ p → □ ◇ p.
+
+Valid in frame iff for every r ← s → u there is r → v ← u.
+
+## Program correctness
+Prove that a program meets its specification.
+
+Correctness specification: formal description of how program is supposed to behave
+
+Program is correct: its executions satisfy the specification
+
+### Verification - Hoare approach
+Prove statements of form `{precondition} program {postcondition}`
+- pre/postcondition are formulas
+- program is a while-program
+- we have proof rules for showing {φ} α {ψ}
+
+Partial correctness: if program starts satisfying φ, and if it halts, then when it halts ψ is satisfied
+
+Total correctness: partially correct, and terminates whenever started while satisfying φ
diff --git a/content/advanced-logic-notes/lecture-9/index.md b/content/advanced-logic-notes/lecture-9/index.md
@@ -11,6 +11,10 @@ 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
+Truth and validity:
+
+
+
Right-linearity:
- "all future points are related"
- definition: ∀ x,y,z: (x < y) ∧ (x < z) → (y < z) ∨ (y = z) ∨ (z < y)
diff --git a/content/advanced-logic-notes/lecture-9/truth-and-validity.png b/content/advanced-logic-notes/lecture-9/truth-and-validity.png
Binary files differ.
