Named Models in Coalgebraic Hybrid Logic (bibtex)

by Lutz Schröder and Dirk Pattinson

Abstract:

Hybrid logic extends modal logic with support for reasoning about individual states, designated by so-called nominals. We study hybrid logic in the broad context of coalgebraic semantics, where Kripke frames are replaced with coalgebras for a given functor, thus covering a wide range of reasoning principles including, e.g., probabilistic, graded, default, or coalitional operators. Specifically, we establish generic criteria for a given coalgebraic hybrid logic to admit named canonical models, with ensuing completeness proofs for pure extensions on the one hand, and for an extended hybrid language with local binding on the other. We instantiate our framework with a number of examples. Notably, we prove completeness of graded hybrid logic with local binding.

Reference:

Lutz Schröder and Dirk Pattinson: Named Models in Coalgebraic Hybrid Logic, In Jean-Yves Marion, Thomas Schwentick, eds.: 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010, Leibniz International Proceedings in Informatics, vol. 5, pp. 645–656, Schloss Dagstuhl - Leibniz-Center of Informatics; Dagstuhl, Germany, 2010. [preprint]

Bibtex Entry:

@InProceedings{SchroderPattinson10,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Named Models in Coalgebraic Hybrid Logic},
  year = {2010},
  editor = {Jean-Yves Marion and Thomas Schwentick},
  booktitle = {27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010},
  publisher = {Schloss Dagstuhl - Leibniz-Center of Informatics; Dagstuhl, Germany},
  series = {Leibniz International Proceedings in Informatics},
  volume = {5},
  pages = {645--656},
  keywords = {coalgebra modal logic named models pure completeness local binding},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/namedModels.pdf"> [preprint] </a>},
  abstract = {  Hybrid logic extends modal logic with support for reasoning about
  individual states, designated by so-called nominals. We study hybrid
  logic in the broad context of coalgebraic semantics, where
  Kripke frames are replaced with coalgebras for a given functor, thus
  covering a wide range of reasoning principles including, e.g.,
  probabilistic, graded, default, or coalitional
  operators. Specifically, we establish generic criteria for a given
  coalgebraic hybrid logic to admit named canonical models, with
  ensuing completeness proofs for pure extensions on the one hand, and
  for an extended hybrid language with local binding on the other.
  We instantiate our framework with a number of examples.
  Notably, we prove completeness of graded hybrid logic with local
  binding.
},
}