行动的逻辑（二）

3.1 程序推理

程序验证有着悠久的历史。自从计算机及其编程诞生以来，研究人员就开始考虑分析程序的方法，以确保它们做了它们应该做的事情。 20 世纪 60 年代，程序正确性的真正数学理论的发展开始初具规模（de Bakker 1980, 466）。值得注意的是，约翰·麦卡锡（John McCarthy）的工作在这里发挥了重要作用，他区分和研究了“国家”等基本概念，McCarthy 1963a，当我们稍后转向人工智能领域时，我们也会遇到他。这一方面导致了编程语言语义领域的发展，另一方面导致了 Floyd (1967)、Naur (1966)、Hoare (1969) 和 Dijkstra (1976) (de Bakker 1980) 在程序正确性方面的重大进展。 。 Floyd 和 Naur 使用基本的逐步归纳原理和附加到程序点的谓词来表达命令式程序的不变属性 (Cousot 1990, 859)、从基本赋值语句（算术表达式到程序变量）构建的程序，并且可以由顺序、条件和重复组成。虽然 Floyd-Naur 方法（称为归纳断言方法）产生了验证条件的系统构造，是一种通过逻辑来证明程序正确性的方法，但它本身并不是严格意义上的逻辑。 。霍尔为程序的正确逻辑铺平了道路，他的组合证明方法导致了现在所谓的霍尔逻辑。通过利用（命令式）程序的句法结构，Hoare 能够将 Floyd-Naur 方法转变为真正的逻辑，其中断言称为形式为 {P}S{Q} 的 Hoare 三元组，其中 P 和 Q是一阶公式，S 是上面提到的命令式编程语言中的程序语句。预期的解读是，如果 P 在语句 S 执行之前成立，那么 Q 在 S（执行）终止时成立。（S 的执行是否终止的问题可以有条件地放入这个霍尔三元组的解读中（部分正确）或无条件（完全正确），从而产生不同的逻辑，参见 Harel 等人 2000）。为了给人以霍尔式逻辑的印象，我们在这里给出了一些简单编程语言的规则，包括对算术表达式的变量赋值，并包含顺序 (;)、条件 (IF) 和重复 (WHILE) 组合。

{P}S1{Q}，{Q}S2{R}{P}S1； S2{R}

{P∧B}S1{Q},{P∧ØB}S2{Q}{P}IFBTHENS1ELSES2{Q}

{P∧B}S{P}{P}WHILEBDOS{P∧ØB}

后来普拉特和哈雷尔将霍尔逻辑推广到动态逻辑（Pratt 1976, Pratt 1979a, Harel 1979, Harel 1984, Kozen and Tiuryn 1990, Harel et al. 2000），人们认识到[1]它实际上是一种形式通过将程序 S 的输入输出关系视为 Kripke 式语义意义上的可访问性关系来实现模态逻辑的研究。[2] 霍尔三元组 {P}S{Q} 在动态逻辑中变为以下公式：P→[S]Q，其中 [S] 是与程序的输入输出关系相关联的模态框运算符（与程序的输入输出关系相关联的可访问性关系） S.动态逻辑的命题版本，PDL，由 Fischer 和 Ladner (1977) 提出，它本身就成为一个重要的研究课题。 PDL 的关键公理是归纳公理

[S*](P→[S]P)→(P→[S*]P)

其中*代表迭代运算符，S*表示程序S的任意（有限）次数的迭代。该公理表示，如果在S的任意次数的迭代之后，P的真实性通过S的执行而被保留，那么，如果P 在当前状态下为真，在 S 进行任意次数的迭代后也为真。Hennessy 和 Milner 引入了一种较弱形式的 PDL，称为 HML，仅具有原子动作框、菱形和命题连接词来进行推理关于并发进程，特别是分析进程等效性（Hennessy 和 Milner 1980）。

这里还值得一提的是，Dijkstra（1976）关于最弱前提条件微积分的工作与动态逻辑（以及霍尔逻辑）密切相关。事实上，Dijkstra 所说的最弱自由前提条件，表示为 wlp(S,Q)，与动态逻辑中的框运算符相同：wlp(S,Q)=[S]Q，而他的最弱前提条件，表示为 wp( S,Q) 是其完全正确性变体，这意味着该表达式还需要语句 S 的终止（Cousot 1990）。

后来人们意识到动态逻辑的应用超出了程序验证或程序推理的范围。事实上，它构成了一般行动的逻辑。 Meyer 2000 中给出了动态逻辑的许多其他应用，包括道义逻辑（另请参见 Meyer 1988）、数据库更新推理、推理系统的语义（例如反射体系结构）。顺便说一句，我们在这里注意到，Meyer 1988 中提出的将动态逻辑用于道义逻辑需要对动作语言进行扩展，特别是添加“动作否定”运算符。该运算符相当有争议的性质引发了对动作否定本身的研究（例如，参见 Broersen 2004）。下面我们在指定智能代理时也会遇到人工智能中动态逻辑的使用。

到目前为止，逻辑足以推理应该终止并显示某种输入/输出行为的程序。然而，到了七十年代末，人们开始意识到也有一些节目不是这样的。反应式程序旨在对理论上可能是无限的输入流做出反应，从而显示出理想的不间断行为。这里并不涉及太多的输入输出行为，而是程序随时间的变化行为。因此，Pnueli（1977）基于时间逻辑的思想，为这种编程风格提出了一种不同的程序推理方式，即： （线性时间）时态逻辑。 （由于反应性通常涉及并发或并行编程，因此时序逻辑通常与这种编程风格相关联。但是，应该指出的是，一系列研究继续将霍尔逻辑的使用扩展到并发程序（Lamport 1977，Cousot 1990， de Roever et al. 2001）。）线性时间时序逻辑通常具有时序运算符，例如下一次、总是（将来）、某个时间（将来）、直到和此后。

时序逻辑与动态逻辑和霍尔逻辑之间的一个有趣区别在于，前者是文献中所谓的内生逻辑，而后者是所谓的外生逻辑。如果程序在逻辑语言中是显式的，则逻辑是外生的，而对于内生逻辑则不是这种情况。在诸如时间逻辑之类的内生逻辑中，程序被假定为固定的，并且被认为是解释逻辑的结构的一部分（Harel et al. 2000, 157）。外生逻辑是组合的，具有允许通过结构归纳进行分析的优点。后来普拉特（Pratt，1979b）尝试将时间逻辑和动态逻辑融合到他所谓的过程逻辑中，这是一种用于推理时间行为的外生逻辑。

目前，计算机科学中应用的时序逻辑领域已经发展成为一个完整的子领域，包括（半）自动推理和模型检查的技术和工具（参见 Emerson 1990）。此外，还提出了基本线性时间模型的变体进行验证，例如分支时间时序逻辑（特别是逻辑 CTL（计算树逻辑）及其扩展 CTL*（Emerson 1990），其中人们可以推理明确地关于非确定性计算中的替代路径（量化），最近还有 CTL 的扩展，称为交替时间时序逻辑（ATL），其模式表示一组代理有一个联合策略来确保其论证，这些系统的行为也取决于其环境的行为，请参阅 Alur 等人 1998。

最后，我们提到了推理程序的另一种逻辑，即。定点逻辑，以所谓的 μ 演算为典型例子，可以追溯到 Scott 和 de Bakker (1969)，并在 Hitchcock 和 Park 1972、Park 1976、de Bakker 1980 和 Meyer 1985 中得到进一步发展。基本运算符是最小定点运算符 μ，捕获迭代和递归：如果 phi(X) 是具有自由关系变量 X 的逻辑表达式，则表达式 μXphi(X) 表示最小 X，使得 phi(X)=X，如果这样存在 X。 μ 演算的命题版本，称为命题或模态 μ 演算，包含命题结构 → 和 false，以及原子（动作）模态 [a] 和 μ 运算符，由命题模态逻辑加上公理 phi[ 完全公理化X/μXψ]→μXψ，其中 ψ[X/Y] 代表表达式 ψ，其中 X 被 Y 代替，并且规则

ψ[X/ψ]→ψ{μXψ→ψ}

（Kozen 1983，Bradfield 和 Stirling 2007）。众所周知，这种逻辑包含 PDL（参见 Harel 等人，2000 年）。

4. 人工智能的行动逻辑

在人工智能（AI）领域，其目标是设计基于计算机的具有智能行为的工件（目的是理解人类智能或只是制作智能计算机系统和程序）。为了实现这一目标，人工智能内部有一个传统，即尝试基于所有相关因素的符号表示来构建这些系统。这种传统被称为符号人工智能或“优秀的老式”人工智能（GOFAI）。在这一传统中，知识表示（KR）的子领域显然非常重要：自人工智能诞生以来，它就发挥了重要作用，并且已经发展成为自己的一个重要领域。 KR 的突出领域之一涉及行动的表示，这些行动由要设计的系统本身或其环境中的参与者执行。当然，除了纯粹的表示之外，关于动作的推理也很重要，因为表示和使用这些表示的推理被认为在 KR 中紧密相连（有时也称为 KR&R，知识表示和推理）。 AI中的相关，最新的发展是基于（智能）代理，一个自主行动实体的概念来基于智能系统的构建，从本质上讲，行动的逻辑在获得一个方面起着至关重要的作用逻辑描述和规范。

4.1代表和推理行动

如上所述，与他们一起推理的行动和形式主义/逻辑的代表是AI，尤其是KR领域的核心。关于AI中有关行动的推理的文献中，一个人比主流计算机科学中遇到的主要问题之一是发现了所谓的框架问题（McCarthy and Hayes 1969）。尽管诸如Dennett（1984）之类的哲学家已将这个问题推广到与行动有关的财产的一般性问题，但问题的核心是，在“常识”环境中，作为AI中的一个人，几乎不可能通过关注的行为来指定所有效果，尤其是所有无效的影响。例如，给定动作，请考虑如果执行该动作，什么不发生，而在通常的情况下，后者比前者难以生产得多，导致大型，复杂的尝试来指定非效应。但是，当然还有相关问题：哪些方面与手头的问题有关；我们需要考虑哪些属性？特别是，这也涉及一项行动的先决条件，该行动可以保证成功的绩效/执行。同样，在常识性环境中，这些是可怕的，一个人总是可以想到应纳入的另一种（前）条件。例如，要成功启动汽车的电动机，应该有一个充电的电池，足够的燃料，…，但也不是太冷的天气，甚至不是足够的手指，以便能够转动起始钥匙汽车中的电动机，…等。尽管此问题引起了所谓的不可行或非单调解决方案，例如默认解决方案（“通常是汽车有电动机”），这本身就产生了一个全新的AI领域，称为非单调或常识性推理，但这是除了本条目的范围之外（我们将有兴趣的读者参考Thomason（2003）在本百科全书中的文章）。我们将重点放在一个不吸引非单调性（直接）的解决方案上。

Reiter（2001）提出了一个（部分）的解决方案，称为“情况”微积分，该框架在KR中非常受欢迎，尤其是在北美，自AI的创始人之一John McCarthy提出以来（McCarthy 1963b，1963b，Mccarthy of tathers of。麦卡锡（McCarthy）1986）。情况演算是一阶逻辑的方言，具有一些温和的二阶特征，尤其是为了推理动作。 （其独特的特征之一是在对象语言中纳入句法实体（“情况”）的所谓语义概念（以及可能的世界（以及真理谓词））的所谓语义概念。）这个空间的条目和原因，我们将尝试在（一阶）动态逻辑中渲染Reiter的想法，或者更确切地说是对其进行略微扩展。 （我们需要动作变量来表示动作变量和动作（或动作表达式）之间的行动表达和平等性，以及（宇宙）对动作变量的量化）。

所谓的Reiter对框架问题的解决方案假设了一个所谓的封闭系统，也就是说，所有（相关的）动作和可变属性的系统（在这种情况下，通常称为“流利”以强调其随着时间的变化性）。通过这个假设，可以表达（非）变化，这是由于执行行动以及对先决条件的检查问题，以确保以非常简洁而优雅的方式确保成功的表现，并以所谓的形式的继任状态公理

（∀a）[POSS（a）→（（[a] f（x））↔（γ+f（x，a）∨（f（x）∧γ -f（x，x，a）））]]]]]

如果A是动作变量，而γ+F（x，a）和γ -f（x，a）是“简单”表达式，而没有动作方式，则表达了ϕ的条件，分别表达了ϕ的条件。因此，非正式地读取该公式，因为在与动作A有关的某些前提条件下，流利的（谓词）f成为参数x的正确，并且仅当条件γ+f（x，a）持有或f（ x）保留（执行a之前）和条件γ -f（x，a）（x，a）（这会导致其变为false）无法保持。此外，表达式（a）在这种公理中示意性地使用，其中整个动作理论应与形式的所谓先决条件公理相辅相成，以ϕa→pos（a）用于混凝土表达式ϕa，以表明成功的实际预先条件执行A

为了了解这在实践中的工作方式，我们考虑了一个域中的一个示例，在该域中，我们的花瓶V可能会被打破或不损坏（因此我们将“破碎”作为一种流利的），而动作掉落和修复。我们还假设（不可变的）谓词易碎物体，并握住对象。现在，继任状态公理变成

（∀a）[poss（a）→（[a]损坏（v）↔（（a = drop（v）∧fragile（v））∨（browt（v）∧a≠修复（v）））]]]

作为前提公理，我们握住了（x）→pos（drop（x））和损坏（x）→pos（修复（x））。该行动理论非常简洁：每个动作只需要一个术语公理和一个前提公理。

最后，在本小节中，我们必须提及有关行动和变革推理的其他一些知名方法。事件演算（Kowalski and Sergot 1986，Shanahan 1990，Shanahan 1995）和流利的微积分（Thielscher 2005）是在情况计算中基于情况的动作表示的替代方法。读者还引用了Sandewall和Shoham 1994的历史和方法论问题，以及与非单调推理的关系。这些想法导致了非常有效的计划系统（例如Talplanner，Kvarnström和Doherty 2000）和实用方法来编程机器人代理（例如，基于情况计算的Golog家族（Reiter 2001），以及Flux（Thielscher 2005）基于流利的演算）。

4.2智能代理的描述和规范

在过去的二十年中，智能代理的概念已成为讨论人工智能理论和实践的统一概念（参见Russell and Norvig 1995，Nilsson 1998）。简而言之，代理是显示智能/合理性和自治形式的软件实体。他们能够主动行动并做出决定，而无需直接控制人类用户。在本小节中，我们将看到（作用的逻辑）如何用来描述 /指定代理的（所需）行为（参见Wooldridge 2002）。首先，我们专注于单个代理商，然后我们转向具有多个代理的设置，称为多代理系统（MAS）甚至代理社会。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。