Thema3465: Unterschied zwischen den Versionen

Aktuelle Version vom 29. November 2016, 22:34 Uhr

Hybrid Logic in the Calculus Structures

Masterarbeit von Armin Troy

Betreuer Steffen Hölldobler
Wissensverarbeitung
09. Mai 2008 – 09. Mai 2008
Download

Hybrid logic is an extension of modal logic which allows to access the states of a

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.

@@ Zeile 8: / Zeile 8: @@
 |Forschungsgruppe=Wissensverarbeitung
 |Abschlussarbeitsstatus=Abgeschlossen
+|Beginn=2008
 |Abgabe=2008
 |Ergebnisse=Troy thesis.pdf
+|Beschreibung DE=Hybrid logic is an extension of modal logic which allows to access the states of a
+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.
+|Beschreibung EN=Hybrid logic is an extension of modal logic which allows to access the states of a
+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.
 }}