| Project/Area Number |
19F19797
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 外国 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
佐野 勝彦 北海道大学, 文学研究院, 准教授 (20456809)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
VIRTEMA JONNI 北海道大学, 文学研究院, 外国人特別研究員
|
|---|
| Project Period (FY) |
2019-11-08 – 2021-03-31
|
| Project Status |
Discontinued (Fiscal Year 2020)
|
| Budget Amount *help |
¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 2020: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 2019: ¥600,000 (Direct Cost: ¥600,000)
|
|---|
| Keywords | 有限モデル理論 / 計算機科学における論理 / 様相モデル理論 / 論理の計算量 / 実数計算の記述計算量 / ハイパー性質のための論理 / 直観主義 inquisitive logic の定義可能性 / Team Semantics / BSS Machines / Modal Logic / Hyperproperties |
|---|
| Outline of Research at the Start |
チーム意味論(Team Semantics)は様々な科学においてみられる依存性・独立性の異なる諸概念をモデル化し研究するための最新の論理的枠組みである。近年盛んに研究されているのは、確率チーム意味論が、有限モデル理論や（BSS機械による）実数計算とどのような関連をもつか、である。これまでの確率チーム意味論は一階述語論理の設定で考察されていたけれども、本研究ではこれを命題論理や様相命題論理の設定で考察し、実数計算のBSSモデルとどのような関連があるのか、をモデル理論、証明論の観点から明らかにする。
|
| Outline of Annual Research Achievements |
研究分担者の、本年度の主要な研究成果は計算機科学のトップ国際会議である Logic in Computer Science に論文がアクセプトされたことである。この研究は有限モデル理論と記述計算量という計算量理論の両方に関するもので、Separate Branching Blum-Shub-Smale 機械 (S-BSS 機械と略記)という Blum-Shub-Smale 機械の代替を定義し、このS-BSS機械を使って非決定的かつ多項式時間で決定できる言語のFaginに由来する論理的な特徴付け（確率独立（一階述語）論理による）を与えた。ここでBSS機械は実数を入力としてとり、１ステップで実数上の算術的演算を行うことができるチューリング機械とみなせる。S-BSS機械はBSS機械よりも実数を計算する仕方がより制限されている。分担者が国際会議CSL (Computer Science Logic)で発表した論文は、LICS論文での結果を、計算量クラスPTIMEに関する結果へと拡張した。さらにこういった結果を命題論理の設定で考察する準備的研究を受入研究者と行った。さらに、昨年度に着手した、実行トレースについてのhyperpropertyをモデルするのに役立つ、チーム意味論をもつ様相論理の研究については論文執筆を行った。分担者の論文 ``On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic''では、二階QBFがホーン節やそれに関連する断片に制限された場合の計算量の特徴付けの結果を得た。受入研究者と分担者は受入研究者の直観主義 inquisitive logic についての結果で残された表現力の分離と標準形に関する二つの未解決問題を肯定的に解決した。
|
| Research Progress Status |
令和2年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和2年度が最終年度であるため、記入しない。
|
