2020 Fiscal Year Research-status Report
Mathematical foundations for the reconfiguration paradigm
| Project/Area Number |
20K03718
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 助教 (80595778)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | institution / hybrid logic / dynamic logic / forcing / omitting types theorem |
|---|
| Outline of Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Everything is going according to the initial plan, which is described in the application in detail.
|
| Strategy for Future Research Activity |
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.
|
| Causes of Carryover |
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.
|
