Model Theory and proof theory of probabilistic logic in propositional and modal team semantics

点击翻译按钮获取中文摘要

研究分担者の、本年度の主要な研究成果は計算機科学のトップ国際会議である 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 についての結果で残された表現力の分離と標準形に関する二つの未解決問題を肯定的に解決した。