行為論理（エージェント論理）とも呼ばれる行為の論理、または行為主体性の論理は、哲学論理学と計算機科学における論理学の一分野であり、エージェント、その行為、およびその能力の形式的表現を研究する。狭義には、行為論理は、エージェントが何かを行う、何かを行うことができる、または何かが成り立つことを確認することを表現する原始演算子を持つ形式体系である。これらの論理は、エージェントと行為にインデックス付けされた様相を追加することで様相論理を一般化し、エージェントが何を達成できるか、その選択がどのように相互作用するか、そして何をもたらすかについての精密な推論を可能にする。
この分野は中世哲学と現代論理学にルーツを持ち、人工知能、プログラム検証、自然言語の意味論などの分野で中心的な役割を果たすようになった。行為論理は、知的エージェント、計画システム、マルチエージェント相互作用をモデル化するための厳密な枠組みを提供し、計算における理論的および応用的研究の両方に不可欠である。
用語と範囲
形容詞「agentive」はラテン語の agens（「行為する者」）に由来し、元々は動詞の文法的行為者を指していた。論理的な文脈では、一次引数位置が命題のみではなくエージェントである演算子または述語を指定し、例えば \(A_i\varphi\)（「エージェント \(i\) が \(\varphi\) を行う」）や \(C_i\varphi\)（「エージェント \(i\) が \(\varphi\) をもたらすことができる」）などがある。
現代の文献では、行為論理は、聖アンセルムスの facere（「行う」）に関する様相説明の形式的再構成のために狭義に使用されることがある。より広義には、この用語は行為の論理または行為主体性の論理と互換的に使用され、行為と選択の構造を捉えるために設計された様相論理と動的論理のファミリーを網羅する。この広義の用法は、哲学、言語学、計算機科学で開発されたシステムを含み、すべて論理形式の明示的要素としてのエージェントに焦点を当てている。
歴史的背景
中世および近世のルーツ
中世の論理学者は、特に義務と権力の議論において、行為の様相と可能性や必然性などの真理様相との間の類似性をすでに探求していた。影響力のある初期の行為分析は、聖アンセルムス（11世紀）によるもので、彼は「\(\varphi\) を行う」ことを命題上の様相演算子の一種として扱い、後の行為の様相論理を先取りした。アンセルムスの理論の現代的な再構成は、結果として得られる行為論理が近傍意味論でモデル化でき、認識可能な対当の正方形を満たすことを示している。
現代の行為の論理
行為の論理の現代的研究は、20世紀半ばに義務論理と時制論理の発展と並行して始まった。初期のシステムは、ゲオルク・ヘンリク・フォン・ウリクト、スティグ・カンガーらによって提案され、しばしば規範と責任に関する疑問によって動機付けられた。1960年代以降、2つのほぼ独立したが最終的に収束する伝統が出現した：可能な未来の間でのエージェントの選択を強調する分岐時間の伝統（STIT論理で頂点に達する）、およびプログラムと行為の動的論理（計算機科学内でプログラム実行の推論のために開発された）。
1990年代と2000年代には、行為論理は、AIにおける知識表現、計画、マルチエージェントシステム、および言語学における動的意味論と更新意味論に関連してさらに発展した。これらの発展は、哲学、理論計算機科学、AIからの洞察を統合し、豊かな学際的分野を創り出した。
核心的な考え方
多様性にもかかわらず、ほとんどの行為論理はいくつかの一般的なテーマを共有している。エージェントは、\([i\ {\sf does}]\varphi\) や \(C_i\varphi\) のように、様相演算子の明示的インデックスとして扱われる。行為は、到達可能性関係に沿った可能世界間の変化を介して暗黙的に、または原始的および複合的行為を表す項として明示的に表現される。選択と能力は、エージェントが何を保証できるかを記述する様相によって捉えられ、通常は環境や他のエージェントに関する仮定に相対的である。
合成の下での閉包性、異なるエージェント間の相互作用、義務（エージェントが何をすべきか）や知識（エージェントが何をする方法を知っているか）との接続などの形式的性質が調査される。これらの核心的な考え方は、異なるシステムを比較し、実際的な問題に適用するための共通の枠組みを提供する。
STIT論理
STIT（「sees to it that」）論理は、ヌエル・ベルナップらによる研究に起源を持ち、分岐時間の枠組みで行為主体性を扱う。STITモデルは、木構造を持つ部分的に順序付けられた瞬間の集合、歴史（木を通る最大分岐）の集合、および各瞬間の各エージェントについて、そのエージェントが利用できる選択を表すその瞬間を通る歴史の分割から構成される。
直感的には、瞬間におけるエージェントの行為は、どの同値類（選択セル）の歴史が現実になるかを決定する；式 \([i\ {\sf stit}:\varphi]\) は、歴史-瞬間ペアで、\(\varphi\) がエージェントの現在の行為に対応する選択セル内のすべての歴史で成り立つ場合に真である。異なるSTIT演算子が区別されており、特にチェラスSTIT演算子（しばしば \([i\ {\sf cstit}:\varphi]\) と書かれる）と、エージェントの選択が \(\varphi\) の真理に違いをもたらすという条件を追加する熟考的STIT演算子がある。これらの演算子は、エージェントが一緒に行動する場合や、あるエージェントの行為が別のエージェントの行為を妨げる場合を含む、個人および共同の行為主体性についての精密な推論を可能にする。
STIT論理は、義務推論、ゲーム理論、責任と因果関係の分析に適用されてきた。それらは動的環境での選択と能力をモデル化するための堅牢な枠組みを提供し、AIにおけるマルチエージェントシステムの研究に影響を与えてきた。
行為の動的論理
1970年代以降に計算機科学で開発された動的論理は、行為をプログラムとして表現し、様相 \([\alpha]\varphi\) と \(\langle\alpha\rangle\varphi\) を持ち、これはおおよそ行為 \(\alpha\) のすべての（それぞれ、いくつかの）実行後に \(\varphi\) が成り立つことを意味する。これらの論理は元々プログラム検証のために設計され、プログラム実行の状態への影響についての推論を可能にした。
行為の文脈では、動的論理は行為を項として明示的にモデル化し、合成、選択、反復演算子を持つ。これにより、行為のシーケンス、条件付き行為、反復行為などの複雑な行為構造の表現が可能になる。行為の動的論理は、計画、ロボティクス、自然言語の意味論に適用され、行為文や命令文の意味を捉えている。
人工知能への応用
行為論理は、人工知能における行為の推論、計画、知的エージェントのための形式主義を支えている。それらは、エージェントの知識、能力、目標を表現し、行為が世界をどのように変えるかを推論するための形式的基盤を提供する。計画では、行為論理は行為の前提条件と効果を指定するのに役立ち、代替計画とその結果についての推論をサポートする。
マルチエージェントシステムでは、行為論理は協力、競争、通信を含むエージェント間の相互作用をモデル化する。それらはプロトコルの指定、分散システムの性質の検証、戦略的行動の分析に使用される。大規模言語モデルや他の機械学習システムの開発も、研究者が自身の行為や他者の行為について推論できるエージェントを構築しようとする中で、行為の概念を利用している。
他の論理との関係
行為論理は、様相論理、義務論理、時相論理と密接に関連している。それらはエージェントにインデックス付けされた様相を追加することで様相論理を拡張し、時間の経過に伴う変化を表現するために時相演算子を組み込むことが多い。義務と許可を推論する義務論理は、行為論理と組み合わせて、エージェントが何をすべきか、または何を許可されているかを表現できる。線形時相論理や計算木論理などの時相論理は、行為のシーケンスと分岐する未来についての推論の基盤を提供する。
行為論理と知識との接続も重要である。エージェントが何を知っているかを推論する認識論理は、行為論理と統合して、エージェントが何をする方法を知っているか、または何を達成できるかを知っているかを表現できる。この統合は、エージェントが自身の知識と能力について推論しなければならないAIでの応用にとって重要である。
関連項目
- 様相論理
- 義務論理
- 時相論理
- マルチエージェントシステム