Forcing and Calculi for Hybrid Logics

研究成果: Contribution to journalArticle査読

3 被引用数 (Scopus)


The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.

ジャーナルJournal of the ACM
出版ステータス出版済み - 8 6 2020

All Science Journal Classification (ASJC) codes

  • Software
  • Control and Systems Engineering
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence

フィンガープリント 「Forcing and Calculi for Hybrid Logics」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。