commit d397509a0995611c7255e48403bf23cf38a8bba6 parent f07aa866ac886d5053ff42bcbb10277e163801b4 Author: Alex Balgavy <alex@balgavy.eu> Date: Sat, 26 Mar 2022 12:59:46 +0100 Advanced logic: some typos Diffstat:
5 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/content/advanced-logic-notes/epistemic-logic.md b/content/advanced-logic-notes/epistemic-logic.md @@ -7,6 +7,6 @@ title = 'Epistemic logic' - [i] φ: 'agent i knows that φ is true' (also written Kᵢφ) - 〈i〉φ: 'agent i considers φ possible' -In an epistemic frame, the relation statemtn sRᵢt means: given his information in situation s, agent i considers t possible +In an epistemic frame, the relation statement sRᵢt means: given his information in situation s, agent i considers t possible diff --git a/content/advanced-logic-notes/exercise-1/index.md b/content/advanced-logic-notes/exercise-1/index.md @@ -173,6 +173,6 @@ digraph g { </details> -We cannot influence falsifier here since we play as verifier (trying to show that it hols). +We cannot influence falsifier here since we play as verifier (trying to show that it holds). But no matter what falsifier does, verifier has a winning strategy. diff --git a/content/advanced-logic-notes/proof-systems-and-derivation/index.md b/content/advanced-logic-notes/proof-systems-and-derivation/index.md @@ -20,7 +20,7 @@ Admissible rule: Proof system K is sound and complete with respect to all frames, ⊢K φ iff ⊨ φ. -Soundness and completeness results (**note:** the frame classes _do_ need to be memorized) +Soundness and completeness results (**note:** the frame classes _need_ to be memorized) - K sound and complete for all frames - T sound and complete for all _reflexive_ frames - T: K with □ p → p diff --git a/content/advanced-logic-notes/propositional-dynamic-logic-pdl/index.md b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/index.md @@ -11,8 +11,8 @@ Definitions: - program: regular program which slightly generalizes a while program - statement {pre}program{post}: formula pre → [program] post -For every program α we have modality \<α\>: -- \<α\>: it's possible to execute α from current state, and successfully halt in state satisfying φ (like existential quantification) +For every program α we have modality 〈α〉: +- 〈α〉φ: it's possible to execute α from current state, and successfully halt in state satisfying φ (like existential quantification) - [α]φ: for all executions of α, if α successfully halts, then it halts in a state satisfying φ (like universal quantification) Program definitions: @@ -84,7 +84,7 @@ Calculate the relation for `if p then a else b`, which is encoded as `(p?; a) ∠While: - program: `while p do a` -- encoding: (P?; a)\*; ¬ p? +- encoding: (p?; a)\*; ¬ p? <details> <summary>Example</summary> diff --git a/content/advanced-logic-notes/temporal-logic/index.md b/content/advanced-logic-notes/temporal-logic/index.md @@ -38,7 +38,7 @@ 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 + - not true if other options. e.g. you can go directly from Centraal to Utrecht, but Amstel station is still there. - next not definable in basic modal logic Operator until: