マルチモーダルロジック

多様相論理とは、複数の基本様相演算子を持つ様相論理であり、理論計算機科学において重要な応用が見出されている。

概要

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

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

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

注記

  1. ^ セルジオ・テッサリス、エンリコ・フランコーニ、トーマス・アイター (2009). 推論ウェブ. 情報システムのためのセマンティックテクノロジー：第5回国際サマースクール2009、イタリア、ブリクセン＝ブレッサノーネ、2009年8月30日～9月4日、チュートリアル講義. シュプリンガー. p. 112. ISBN 978-3-642-03753-5。
  2. ^ フェレンツィ 2002、257ページ。

参考文献

「https://en.wikipedia.org/w/index.php?title=マルチモーダルロジック&oldid=1293802851」より取得