# Hybrid Logic in the Calculus Structures

## Hybrid Logic in the Calculus Structures

##### Master's thesis by Armin Troy

- Supervisor Steffen Hölldobler
- Wissensverarbeitung
- 2008 – 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.