| 研究課題/領域番号 |
20K03718
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 助教 (80595778)
|
|---|
| 研究分担者 |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | institution / hybrid logic / dynamic logic / forcing / omitting types theorem |
|---|
| 研究実績の概要 |
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. We have provided 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. In order to prove completeness, the paper 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.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
Everything is going according to the initial plan, which is described in the application in detail.
|
| 今後の研究の推進方策 |
Within 2021FY we are planning to study an omitting types theorem (OTT) for hybrid dynamic first-order logic with rigid symbols (i.e. including symbols with fixed interpretations across worlds) and sufficiently expressive fragments. Observe that an OTT for the full logic would not necessarily have given us the property for its fragments, thus the generality of our proof is an important feature. The result will be obtained using model-theoretic forcing.
One application that we provide is a completeness theorem for constructor-based logic, following an analogous classical result for omega-logic. Constructor-based completeness is a modern approach to the well-known ω-completeness, which has applications in formal methods. We make the result independent of the arithmetic signature by working over an arbitrary vocabulary where we distinguish a set of constructors which determines a class of Kripke structures reachable by constructors.
|
| 次年度使用額が生じた理由 |
Initially, I plan to go to TPP2020, NII, WADT2020 and visit Bremen to develop my research, but these events were canceled due to the COVID-19.
In 2021FY, I am planning (1)a visit La Trobe University, (2)a visit to The University of Queensland, (3) an invitation for Prof. Tomasz Kowalski for joint research collaboration, and (4) a participation to an international conference in Europe.
|
