マルチモーダルロジック

マルチモーダル論理は、複数の基本モーダル演算子を持つモーダル論理であり、理論計算機科学で広く応用されています。

n 個の基本単項様相演算子を持つ様相論理は、 n様相論理と呼ばれます。これらの演算子と否定 が与えられれば、の場合に限りとして定義される様相演算子を常に追加して、証明可能な同値性の両方の要素の必然性 (つまり「可能化」) の下でさらに安定している場合 、古典的な多様相論理を与えることができます。${\displaystyle \Box _{i},i\in \{1,\ldots ,n\}}$${\displaystyle \Diamond _{i}}$${\displaystyle \Diamond _{i}P}$${\displaystyle \lnot \Box _{i}\lnot P}$

おそらく、2 様相論理の最初の実質的な例は、アーサー・プライアの時制論理で、2 つの様相 F と P があり、「将来のいつか」と「過去のあるとき」に対応しています。無限に多くの様相を持つ論理^[1]は、1976 年にVaughan Prattによって導入され、すべての正規表現に対して別々の様相演算子を持つ動的論理です。1977年に導入され、プログラム検証を目的とした時相論理のバージョンには、 2 つの様相があり、動的論理の [ A ] 様相と [ A *] 様相に対応し、単一のプログラムAは、宇宙全体が時間的に 1 歩前進すると理解されます。マルチモーダル論理という用語自体は、1980 年まで導入されませんでした。マルチモーダル論理の別の例は、ヘネシー - ミルナー論理で、それ自体がより表現力豊かな様相μ 計算の一部であり、これも固定小数点論理です。

マルチモーダル論理は、ある種の知識表現を形式化するためにも使用できます。認識論的論理の動機は、複数のエージェント（信念や知識を形成できる主体とみなされる）を許可し、各エージェントの信念または知識を管理して、それらについて認識的アサーションを形成できるようにすることです。様相演算子は、各エージェントの認識を記録できなければならないため、エージェントのセットにインデックス付けされている必要があります。動機は、「主体i は、真であることについての知識を持っている」とアサートする必要があることです。しかし、それは「主体i は信じている」を形式化するためにも使用できます。可能世界意味論アプローチに基づく意味の形式化には、クリプキ意味論のマルチモーダル一般化を使用できます。単一の「共通の」アクセス可能性関係の代わりに、エージェントのセットにインデックス付けされた一連の関係があります。^[2]${\displaystyle \Box}$${\displaystyle \Box _{i}}$${\displaystyle \Box _{i}\alpha }$${\displaystyle \alpha}$${\displaystyle \alpha}$

• フェレンチ、ミクロス (2002)。マテマティカイ ロジカ(ハンガリー語)。ブダペスト: ムシャキ・コニフキアド。ISBN 963-16-2870-1。
• Dov M. Gabbay 、Agi Kurucz 、 Frank Wolter、Michael Zakharyaschev (2003)。多次元様相論理：理論と応用。Elsevier。ISBN 978-0-444-50826-3。{{cite book}}: CS1 maint: 複数の名前: 著者リスト (リンク)
• Walter Carnielli、Claudio Pizzi (2008)。『モダリティとマルチモダリティ』 Springer。ISBN 978-1-4020-8589-5。

• スタンフォード哲学百科事典のジェームズ・ガーソンによる「様相論理」の項目