Hybrid Logic in the Calculus Structures
Hybrid Logic in the Calculus Structures
Masterarbeit von Armin Troy
- Betreuer Steffen Hölldobler
- Wissensverarbeitung
- 21. November 2008 – 21. November 2008
- Download
Kripke structure directly from within the logic. This is achieved with nominals which are an additional kind of propositional symbols. Nominals can be used to identify states since they are true at exactly one state of the Kripke structure by definition. The calculus of structures is a type of inference system which does not only allow rule applications at the topmost connective of a formula, as it is the case for classical inference systems like sequent calculus, but also at subformula positions. An inference system in the calculus of structures is presented for a basic hybrid logic which contains the jump-operator @ as its only hybrid operator. A translation between this inference system and two different sequent calculae for hybrid logic is shown.