能动逻辑，亦称行动逻辑或施为逻辑，是哲学逻辑与计算机科学逻辑的一个分支，研究对智能体、其行动及其能力的正式表示。在狭义上，能动逻辑是一种形式系统，其原始算子表达某智能体做了某事、能做某事或确保某事为真。这些逻辑通过添加以智能体和行动为索引的模态词来推广模态逻辑，从而能够精确推理智能体可实现什么、其选择如何相互作用以及它们带来什么结果。
该领域根植于中世纪哲学和现代逻辑，并已成为人工智能、程序验证和自然语言语义等领域的关键。能动逻辑为建模智能体、规划系统及多智能体交互提供了严格框架，使其对计算领域的理论与应用工作都至关重要。
术语与范围
形容词“agentive”源自拉丁语agens（“行动者”），最初指动词的语法施事。在逻辑语境中，它指代那些主要参数位置是智能体而非仅命题的算子或谓词，例如\(A_i\varphi\)（“智能体\(i\)做\(\varphi\)”）或\(C_i\varphi\)（“智能体\(i\)能带来\(\varphi\)”）。
在当代文献中，能动逻辑有时狭义地用于对圣安瑟伦关于facere（“做”）的模态理论的正式重构。更广泛地，该术语与行动逻辑或施为逻辑互换使用，涵盖旨在捕捉行动与选择结构的一系列模态和动态逻辑。这种广义用法包括在哲学、语言学和计算机科学中发展的系统，它们都关注智能体作为逻辑形式的显式元素。
历史背景
中世纪与近代早期根源
中世纪逻辑学家已探索行动模态与诸如可能性和必然性等真势模态之间的类比，特别是在义务与权力的讨论中。一个影响深远的早期能动分析归功于圣安瑟伦（11世纪），他将“做\(\varphi\)”视为命题上的一种模态算子，预示了后来的行动模态逻辑。对安瑟伦理论的现代重构表明，由此产生的能动逻辑可用邻域语义建模，并满足可识别的对立四边形。
现代行动逻辑
对行动逻辑的现代研究始于20世纪中叶，与道义逻辑和时态逻辑的发展并行。早期系统由格奥尔格·亨利克·冯·赖特、斯蒂格·坎格等人提出，通常受关于规范与责任的疑问驱动。从1960年代起，两个基本独立但最终汇合的传统出现：一个是以STIT逻辑为顶峰的分支时间传统，强调智能体在可能未来中的选择；另一个是程序与行动的动态逻辑，在计算机科学中发展以推理程序执行。
在1990年代和2000年代，行动逻辑进一步与知识表示、规划和AI中的多智能体系统，以及语言学中的动态和更新语义相联系而发展。这些发展整合了哲学、理论计算机科学和AI的见解，形成了一个丰富的跨学科领域。
核心思想
尽管存在多样性，大多数能动逻辑共享几个一般主题。智能体被视为模态算子的显式索引，如\([i\ {\sf does}]\varphi\)或\(C_i\varphi\)。行动要么通过可能世界沿可达关系的变化隐式表示，要么作为表示原始和复合行动的项显式表示。选择与能力通过描述智能体能确保什么的模态词捕捉，通常相对于环境和其它智能体的假设。
诸如在复合下的封闭性、不同智能体间的交互，以及与义务（智能体应当做什么）和知识（智能体知道如何做什么）的联系等正式性质被研究。这些核心思想为比较不同系统并将其应用于实际问题提供了共同框架。
STIT逻辑
STIT（“确保”）逻辑，源于努埃尔·贝尔纳普及其合作者的工作，在分支时间框架中处理施为。STIT模型由具有树状结构的偏序时刻集、历史集（通过树的最大分支）以及每个智能体在每个时刻对通过该时刻的历史的划分组成，该划分表示智能体可用的选择。
直观上，智能体在某一时刻的行动决定哪个等价类（选择单元）的历史成为现实；公式\([i\ {\sf stit}:\varphi]\)在历史-时刻对中为真，当且仅当\(\varphi\)在对应于智能体当前行动的选择单元中的所有历史上成立。已区分不同的STIT算子，特别是Chellas STIT算子，通常写作\([i\ {\sf cstit}:\varphi]\)，以及深思性STIT算子，它添加了智能体的选择对\(\varphi\)的真值产生影响的条件。这些算子允许精确推理个体和联合施为，包括智能体共同行动或一个智能体的行动排除另一个的情况。
STIT逻辑已应用于道义推理、博弈论以及责任与因果分析。它们为在动态环境中建模选择和能力提供了稳健框架，并影响了AI中多智能体系统的工作。
行动动态逻辑
动态逻辑，自1970年代起在计算机科学中发展，将行动表示为具有模态词\([\alpha]\varphi\)和\(\langle\alpha\rangle\varphi\)的程序，大致意思是，在行动\(\alpha\)的每次（分别地，某些）执行之后，\(\varphi\)成立。这些逻辑最初设计用于程序验证，允许推理程序执行对状态的影响。
在能动语境中，动态逻辑用于将行动显式建模为项，具有复合、选择和迭代算子。这允许表示复杂的行动结构，如行动序列、条件行动和重复行动。行动动态逻辑已应用于规划、机器人学和自然语言语义，其中它们捕捉行动句和祈使句的意义。
在人工智能中的应用
能动逻辑支撑了人工智能中关于行动推理、规划和智能体的形式主义。它们为表示智能体的知识、能力和目标，以及推理行动如何改变世界提供了正式基础。在规划中，能动逻辑帮助指定行动的前置条件和效果，并支持对替代计划及其结果的推理。
在多智能体系统中，能动逻辑建模智能体间的交互，包括合作、竞争和通信。它们用于指定协议、验证分布式系统的性质和分析战略行为。大型语言模型和其它机器学习系统的发展也借鉴了能动概念，因为研究人员寻求构建能推理自身及他人行动的智能体。
与其它逻辑的关系
能动逻辑与模态逻辑、道义逻辑和时态逻辑密切相关。它们通过添加智能体索引的模态词来扩展模态逻辑，并常纳入时间算子以表示随时间的变化。道义逻辑，推理义务与许可，可与能动逻辑结合以表达智能体应当做什么或被允许做什么。时态逻辑，如线性时态逻辑和计算树逻辑，为推理行动序列和分支未来提供基础。
能动逻辑与知识之间的联系也很重要。认识逻辑，推理智能体知道什么，可与能动逻辑集成以表达智能体知道如何做或知道其能实现什么。这种集成对AI中的应用至关重要，其中智能体必须推理自身知识和能力。
参见
- 模态逻辑
- 道义逻辑
- 时态逻辑
- 多智能体系统