lectures.alex.balgavy.eu

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

_index.md (2063B)


      1 +++
      2 title = 'Advanced Logic'
      3 +++
      4 # Advanced Logic
      5 - [Intro to Modal Logic (operators, frames, models, tautologies)](intro-to-modal-logic-operators-frames-models-tautologies/)
      6 - [Semantics: truth and validity, game semantics for formula validity](semantics-truth-and-validity-game-semantics-for-formula-validity/)
      7 - [Bisimulations](bisimulations/)
      8 - [Model transformations (tree unravelling, bisimulation contraction)](model-transformations-tree-unravelling-bisimulation-contraction/)
      9 - [Formula validity using sequents and tableaux](formula-validity-using-sequents-and-tableaux/)
     10 - [Standard translation: mapping basic modal logic to first-order predicate logic](standard-translation-mapping-basic-modal-logic-to-first-order-predicate-logic/)
     11 - [The finite model property](the-finite-model-property/)
     12 - [Proof systems and derivation](proof-systems-and-derivation/)
     13 - [Temporal logic](temporal-logic/)
     14 - [Multi-modal logic](multi-modal-logic/)
     15 - [Program correctness](program-correctness/)
     16 - [Propositional dynamic logic (PDL)](propositional-dynamic-logic-pdl/)
     17 - [Epistemic logic](epistemic-logic/)
     18 
     19 Worked exercises:
     20 
     21 - [Exercise 1](exercise-1/): validity, game semantics (verifier/falsifier)
     22 - [Exercise 3](exercise-3/): bisimulation game semantics, sequents, tableaux
     23 - [Exercise 4](exercise-4/): derivation in proof systems, temporal logic
     24 - [Exercise 5](exercise-5/): PDL
     25 - [Homework 1](homework-1/): misc topics
     26 - [Some midterm solutions](some-midterm-solutions/): validity, bisimulation, definability in BML
     27 
     28 [Here's my Anki deck](advanced-logic.apkg)
     29 
     30 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.
     31 You can install Graphviz and run e.g. `dot < graph.dot -Tsvg > graph.svg` (also accepts input files as parameters).
     32 Or you can install [PlantUML](https://plantuml.com/), surround the code with `@startdot...@enddot`, and run `plantuml -p -Tsvg < graph.puml > graph.svg`.