BDI Agent编程语言及其理论基础

108最小ERVA理论计算机科学电子笔记70第5期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html18页BDI面向Agent程序设计语言拉斐尔·H Bordinia，1A'lvaroF. Moreirab，2aDepartamentodeInform'aticaTe'orica（INT）InstitutodeInform'atica（II）南里奥格兰德联邦大学CP 15064，91501-970，Porto Alegre，RS，BrazilbDepartamentodeInform'atica（DEIN）CentrodeCienciasExataseTecnologia（CCET）Universidade de Caxias do Sul（UCS）95070-560，Caxias doSul，RS，巴西摘要在本文中，我们考虑了Rao和George Rao基于Bratman的不对称性理论定义的BDI逻辑的九个原则中的每一个，并且我们验证了Rao的AgentSpeak（L）满足哪些原则，这是一种受认知Agent的BDI架构启发的可计算逻辑语言。这与Rao定义AgentSpeak（L）的最初动机一致：弥合BDI代理系统理论和实践之间的差距。 为了证明这一点，我们首先介绍一种特殊的方式来定义AgentSpeak（L）代理的BDI逻辑的信息，动机和审议模式，根据其结构操作语义（我们在最近的一篇论文中介绍这提供了一个框架，可用于研究AgentSpeak（L）代理的进一步属性，为BDI代理编程提供坚实的理论基础1介绍自从Shoham关于面向代理的编程的论文[15]以来，已经提出了许多代理编程语言，遵循各种方法。Con-Golog [3]是一种基于情景演算的并发编程语言，Concurrent MetateM [5]是基于时态逻辑的，[9]基于动态逻辑编程。AgentSpeak（L）[12]基于1现就职于英国利物浦大学计算机科学系。 电邮地址：afmoreira@inf.ufrgs.br2 目前在的联邦大学的里约Grande南， 巴西电邮地址：afmoreira@inf.ufrgs.br2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。BORDINIAND MOR eIRa109BDI（信念-愿望-意图）架构[13]以及PRS [6]和dMARS [8]的更多实践经验其他BDI编程语言都是从AgentSpeak（L）衍生而来的，例如3APL [7]，在某些方面对其进行了改进（例如，处理计划失败）。BDI架构现在渗透到多智能体系统研究的重要部分。这是在使用面向代理的编程语言时需要考虑的一个重要方面。我们选择使用AgentSpeak（L）并以各种方式对其进行扩展;扩展的语言称为AgentSpeak（XL）[1]。选择AgentSpeak（L）是基于它非常简洁和优雅的符号，因为我们发现它比其他BDI启发的编程语言更忠实于BDI架构。在[12]中，Rao不仅为AgentSpeak（L）引入了抽象解释器的操作，而且他还为该语言勾画了一个证明理论，他声称，某些BDI逻辑满足的已知性质此外，他声称，他的翻译和证据系统之间存在一对一的对应关系。事实上，这是他为弥合BDI理论与实践之间的差距而提出的建议然而，据我们所知，这些说法从未得到证实。Rao提到的被某些BDI逻辑满足的性质的例子是被称为不对称命题原理的那些。本文为BDI编程提供了一个更正式的基础，因为它显示了用AgentSpeak（L）编程的任何代理都满足为了做到这一点，我们首先需要正式定义BDI逻辑中可表达的三种心理态度对AgentSpeak（L）代理的意义。这些定义基于 我 们 在 [11] 中 给 AgentSpeak （ L ） 的这 实 际 上 构 成 了 一 个 证 明AgentSpeak（L）的其他BDI性质的框架。最近的出版物已经出现，其中也有兴趣在属性的BDI代理语言。Winiko Mr. et al. [18]，例如，给一种语言形式语义，这种语言具有一些属性，集成了目标的声明性和过程性视图;这可以用于推理目标，以检测和解决它们之间的冲突。最近流行的多智能体方法来构建复杂的计算系统是显着的。然而，面向代理的编程语言仍然需要大量的理论工作，多代理系统社区的实践基础：这是本文的主要下一节给出了AgentSpeak（L）和不对称命题原则的必要背景。第3节给出了我们在第4节中证明AgentSpeak（L）的不对称命题原则的框架。BORDINIAND MOR eIRa1102背景2.1AgentSpeak（L）在Rao在[12]中介绍了AgentSpeak（L）之后，d'Inverno和Luck在[4]中给出了ab解释器和缺失细节的进一步形式化它们的形式化是使用Z形式规范语言完成的正如我们之前提到的，在[11]中，我们为它提供了一个结构化的操作语义。然而，直到最近，还没有可用的AgentSpeak（L）解释器的实现。在 [10] 中 ， 我 们 已 经 展 示 了 在 Sloman 的 SIM AGENT 框 架 [17] 中 运 行AgentSpeak（L）程序这是AgentSpeak（L）解释器的第一个原型实现，我们称之为SIM Speak。SIM Speak中提供了一种机制，用于将AgentSpeak（L）程序转换为SIM AGENT中的运行在[1]中，我们提出了对AgentSpeak（L）的一些扩展对于这个被称为AgentSpeak（XL）的扩展语言，我们已经用C++从头开始实现了一个高效的解释器，它应该很快就会上市。我们现在介绍AgentSpeak（L）的语法和非正式语义的基础知识（更多细节可以在附录A和上面给出的参考文献中找到）。一个AgentSpeak（L）agent基本上是通过指定一组基本信念和一组计划来创建的。基本信念是通常形式的基础原子（例如，忙（线路））。信念集（动态变化）表示代理目前拥有的关于世界的信息环境）。一个计划可以被认为是一系列的步骤（一个行动过程），代理需要执行，以处理一些感知的事件，如稍后所见。AgentSpeak（L）区分了两种类型的目标：成就目标和测试目标。两者都是为信仰而定义的谓词，但前者是以运算符，而后者则以操作符. 当代理需要通过执行动作并可能实现其他（子）目标（例如，！book（tickets））。当代理需要测试是否相关联的谓词是真信念，即，它是否可以与代理人？busy（X））。（与Prolog中一样，变量用大写字母开头表示。信）接下来，引入了触发事件的概念它是AgentSpeak（L）中一个非常有两种类型触发事件：那些与心理态度，特别是信念和目标的增加−忙（线路），+！book（X））。AgentSpeak（L）智能体使用计划来定义可能的行动过程因此，计划必须涉及代理能够对其环境执行的基本操作详细地说，AgentSpeak（L）计划具有头部BORDINIAND MOR eIRa111它由一个触发事件（该计划的目的）和一个信念字面量的连接组成，如果计划要执行，则需要满足该上下文（该上下文必须是该代理人在计划成为意图时的信念基础的逻辑结果）。一个计划也有一个主体，这是一系列基本的行动或目标，代理人必须实现（或测试）。一个示例计划是+concert（X，Y）：like（X）<$busy（line）<-call（Y）;. ;！票（tickets）AgentSpeak（L）解释器还管理一组事件和一组意图，其功能需要三个选择函数。事件选择函数（SE）从事件集合中选择单个事件;另一选择函数（SAp）选择“选项”（即，第三选择功能（SI）从所述意图集合中选择一个选择函数应该是特定于代理的，在这个意义上，它们应该根据代理的特征进行选择因此，我们在这里让选择函数未被定义，因此它们所做的选择应该是不确定的。我们对文献[1]中AgentSpeak（L）的扩展，精确地处理了有效意图选择函数的自动生成。 扩展语言允许人们表达计划之间的关系，以及它们执行的量化标准。然后，我们使用决策理论的任务调度来指导意图选择功能所做的选择。意图是一个主体为了处理某些事件而承诺的特定行动过程每个意图都是一堆部分实例化的计划。当源自于对代理的环境的感知时，可以在计划的执行之后开始的事件可以是外部的基于感知的信念的添加和删除是外部事件）;或内部事件，当从代理自己的计划执行中生成时计划中的子目标是目标的添加，其可以是触发事件）。在后一种情况下，事件伴随着产生它的意图（因为为该事件选择的计划将被推到该意图之上外部事件产生新的意图，代表代理人接下来，我们将详细介绍AgentSpeak（L）解释器的功能在Agent程序的每个解释周期，AgentSpeak（L）更新一个事件列表，这些事件可能是由对环境的感知或意图的执行（当子目标在计划主体中指定时）生成的假设信念是从感知中更新的，并且每当代理的信念发生变化时这个信念修正函数不是AgentSpeak（L）解释器的一部分，而是代理架构的一个必要组件SE选择事件后，AgentSpeak（L）必须统一该事件BORDINIAND MOR eIRa112在计划的头中触发事件这将生成一组所有相关计划。当将该集合中的计划头的上下文部分与代理然后，SAp从该集合选择单个适用的计划（处理该事件的预期手段），并且将该计划推到现有意图的顶部（如果事件是内部意图），或者在意图集合中创建新意图（如果事件是外部的，即，从对环境的感知中产生因此，智能体的每个在这个阶段，剩下要做的就是选择一个单一的意图在那个周期中执行S1函数选择代理的意图之一意图集合内的部分实例化计划的独立堆栈之一在这个意图的顶部有一个计划，它的身体开始的公式被用来执行。这意味着主体在其环境中执行基本动作，生成内部事件（如果子目标是成就目标），或者执行测试目标（这意味着必须检查信念集）。如果意图是执行基本动作或测试目标，则需要更新意图集合。在测试目标的情况下，进一步的变量实例化将发生在包含该测试目标的部分实例化的计划中（并且测试目标本身从其被采取的意图中移除在选择基本动作的情况下，意图集合的必要更新只是从意图中删除该动作（解释器通知负责代理解释器的架构组件需要什么动作当被移除的公式标记子计划的主体的结束时，生成它的子目标（其因此停留在堆栈中紧接在其下方的计划的主体的开始处）也从意图中移除，或者如果初始计划（即，由外部事件触发的计划，因此在意图的底部）是完成执行的计划。这结束了一个执行周期，AgentSpeak（L）重新开始，在代理对其进行操作后检查环境的状态，生成相关的事件，等等。我们在[11]中给出的AgentSpeak（L）的抽象语法和操作语义在附录A中以非常紧凑的方式再现对这些材料的一些熟悉对于理解下一节中的框架和证明是必要的2.2不对称命题原则根据Rao和George Rao [14]，Bratman• 一个行动者既打算做一个行动，又相信它不会做，这是非理性的（意图-信念不一致）;BORDINIAND MOR eIRa113• 对于一个行动者来说，意图做一个动作但不相信它会做它是理性（意图-信念不完全性）。对此，Rao和George Rao补充了这样一个观点：• 一个行动者相信它可以做一个动作而不需要有意图，这是理性的（信念-意图不完全性）。这些由Rao和George Ragin [14]制定为原则AT 1 他们还为其他两对心理态度（意图-欲望和欲望-信念）的组合制定了原则。表1显示了所有九个不对称理论原则。标签原则AT1| = INTEND（意图）Δ T<$BEL（<$ΔT）Δ T 2 | = INTEND（意向）THEBEL（意向）AT 3| = BEL（）INTEND（）AT4| = INTEND（意向）DES（意向）AT 5| = INTEND（意向）终止（意向）AT6 | = DES（DES）AT7| = DES（DES）<$BEL（<$BEL）AT 8| =DES（）BEL（）在9| = BEL（）DES（）表1不对称命题原则[14]。在[14]中，INTEND模态如果被定义在状态公式上，这意味着这里的概念是意图的概念-即（达到环境的某种状态）而不是意图（做一个将导致环境达到某种期望状态的动作因此，读者可能不清楚表1中的BDI公式是否实际上捕获了这不是在本文的范围内讨论：我们感兴趣的是在这里展示如何证明BDI属性在一个实用的编程语言，这九个原则当然表达了有趣的性质BDI代理（无论他们是否准确捕捉布拉特曼BORDINIAND MOR eIRa114⟨⟩3AgentSpeak（L）中BDI性质的证明框架为了证明哪一个不对称命题原则适用于AgentSpeak（L），我们首先需要能够表达AgentSpeak（L）代理的BDI逻辑的三个B-D-I组成部分在附录A中，我们以非常紧凑的方式再现了AgentSpeak（L）代理的语法和结构操作语义，如[11]所示。我们在下面使用附录中给出的关于施动者ag的定义，它实际上是一个信念序列和一个计划序列（在句法规则中是“ag：：= bsps“），以及施动者的环境的一个主体环境C在那里被定义为一个元组I，E，A，R，Ap，i，p，ε，其中在这里只与意图I、事件集合3E和动作集合4A。一个Agent和它的环境形成了一个转换系统的配置，为AgentSpeak（L）提供操作语义。 我们使用符号CI来表示C的I分量，其他分量也是如此。 我们用i，iJ，。。表示意图，i [p]表示计划p在上面的意图，如果i。基于上述主体和主体环境的部分，我们将能够引入BDI逻辑中可表达的三种心理态度的定义（BEL（），DES（）和INTEND（））。在这里，定义三种模态的formulatrix是简单的原子，类似于AgentSpeak（L）语法中的基原子是唯一可以出现在主体的信念基础和外部事件中的公式我们需要正式确定在特定情况下，三种BDI模态对AgentSpeak（L）代理的意义我们从信念模态开始，很简单。定义3.1[相信AgentSpeak（L）智能体]我们说AgentSpeak（L）智能体相信一个公式，它包含在智能体的信念基础中BEL（ε）ε∈ bs.3当信念修正函数（不是AgentSpeak（L）解释器的一部分，而是代理的一般架构的一部分）更新信念库时，相关的事件被包括在这个集合中。也就是说，从感知环境的信念的变化表示为外部事件，包括在这个集合中，以及内部的。请注意，这意味着AgentSpeak（L）解释器与（假设的）整体代理架构的其他部分的交互：信念修订函数在这里插入实际由AgentSpeak（L）解释器处理4至于事件，这提供了AgentSpeak（L）解释器与其他解释器的交互。整个代理体系结构的一部分（在本例中，使用代理的执行器）。这个集合中包含的动作表达式告诉其他架构组件在环境中实际执行相应的动作，从而改变环境。BORDINIAND MOR eIRa115I→I∈ ∈I∈I{}这不需要进一步解释，因为代理的信念在AgentSpeak（L）解释器中显式表示。意图在架构中也是相当明确的，但同样不适用于欲望。这就是为什么我们在欲望之前引入意图模态（也因为我们需要这个定义来定义欲望）。我们首先定义一个辅助函数agoals：P（Φ），其中是所有个体意图的域，Φ是所有原子公式的域（如上所述回想一下，意图是一堆部分初始化的计划，因此，根据附录中计划ps的语法定义，如果pps是计划，则p;如果i，则也是i[p]。. 换句话说，agoals函数接受一个意图，并返回其中计划的触发事件部分中的所有成就目标agoals（i）={}.对于一个yi∈I且p∈ps：当p = +时，求a（i）的值。at：ct<-hagoals（i[p]）=（一）其他情形。如果我们遵循Rao对AgentSpeak（L）语义的原始定义，我们就不需要担心触发事件，而需要在上面的定义中添加成就目标。在意图中（遵循最初的定义），不是成就目标的触发事件只出现在计划的底部。外部事件创造了智能体需要考虑的新的注意力焦点;换句话说，为它们创造了新的意图。只有成就目标的执行（来自计划的主体）会导致增加内部事件，这些事件在被选择时会改变意图。特别是，这些事件所做的是在现有意图的基础上推出（部分实例化的）计划。因此所有计划栈中的触发事件（I中的意图之一）是ad-成就目标的不同版本，除了最底层的一个，这是一个信念的改变（从感知）。然而，在我们在附录A中提供的语义处理计划失败也使得在意图中发现成就目标的删除成为可能，但这不在这里给出的语义中，尽管它在[1]中给出的解释器中实现当意图等待一个合适的子计划被选择时，意图被暂停（以内部事件的形式，这是一个与现有意图相关的事件）;暂停的意图在[4]中得到了明确的形式化。因此，被中止的意图正是在情境C下出现在事件集合CE中的那些意图。也就是说，假设成就目标出现在计划主体的开头，并且该计划位于（通过意图选择功能）选择执行的意图之上在该意图再次被选择执行之前，需要从CE中选择相关事件，并且必须为其找到相关和适用的计划（预期手段）如果发生这种情况，预期的方法将被推到堆栈的顶部，BORDINIAND MOR eIRa116∈ I⟨⟩只有这样（先前暂停的）意图才回到CI，再次成为执行的候选（参见附录中的规则Achieve和IntEv事件的格式是te，i，其中te是触发事件（详见附录），i是产生它的意图（i是外部事件的T）。因此，在情况C下，AgentSpeak（L）代理定义3.2[AgentSpeak（L）智能体中的意图] AgentSpeak（L）智能体在情况C下意图实现，它具有当前出现在其意图集合I中的成就目标，或者是出现在与E中的事件相关联的（暂停的）意图中的成就目标。对于代理人INTEND（意）i∈CIagoals（i）e，iagoals（i）.虽然这在AgentSpeak（L）的原始文献中没有提到，但我们的印象是，AgentSpeak（L）代理中的愿望最好由其事件集内部事件是成就目标5，这显然是愿望：传统上，目标是假设相互一致的愿望的子集[16];在用于AgentSpeak（L）的架构的简化版本中，目标的一致性是理所当然的-参见[18]关于目标冲突的讨论。因此，我们的解释是，CE中具有成就目标的附加形式的事件是欲望（即，它们还没有被选择成为预期的，但是表示代理希望实现的状态）;已经预期的成就目标也是期望的，但是这在下面解释。另一方面，CE中的外部事件回想一下，外部事件被表达为信念的变化;它们是基于对环境的感知的信念修正 外部事件，反过来，导致一系列内部事件：这些我们认为是代理人的愿望（而不是他们的外部原因，这代表了注意力的焦点）。然而，当一个内部事件被选择（并从事件集合E中删除）以试图为其找到相关和适用的计划时，其中一个计划成为处理该事件的预期手段，这并不意味着代理不再希望处理该事件。一种可能的解释是，只有当在意图集合中与之相关的计划的执行结束时，它才不再是一种愿望事实上，这是一个常见的解释，意图是一个子集的代理人的愿望（当一个人正在考虑的意图，而不是意图，当然）。因此，除了E中的成就目标之外，我们还将智能体的所有意图视为智能体的愿望。重要的是要强调，通过这种解释的选择5再次，在我们的语义中，由于扩展允许计划中的信念变化，内部事件也可以是信念的添加和删除，但不是在原始语义中BORDINIAND MOR eIRa117对于欲望在AgentSpeak（L）代理中的含义，我们正在确定AgentSpeak（L）代理将满足不对称命题原则AT4、AT5和AT6中的哪一个（这些原则与欲望和意图有关）然而，我们认为这是最合理的解释，因为意图通常被视为代理人承诺采取行动以实现它们的那些愿望（因此意图确实是愿望的子集）。定义3.3[AgentSpeak（L）agents中的欲望]在情况C下的一个agent需要一个公式，公式i是C的一组事件E中的一个成就目标DES（）+！i∈ CEINTEND（）.在定义了如何解释AgentSpeak（L）的BDI逻辑的信念、愿望和意图模态，我们准备开始证明AgentSpeak（L）代理满足哪些不对称命题原则。4AgentSpeak（L）的非对称命题原则的证明我们首先提出三个引理，每个引理都涉及到不对称性原则（ATP），这些原则指的是成对采取的BDI态度之间的关系。关于三个原则AT 1-AT 3（与信念和欲望相关）的论证如果AgentSpeak（L）程序员调用某个成就目标！如果所有的行为都是基于行为的，那么他们期望行为被代理相信（通过对环境的感知），这是一种很好的编程风格。与选择处理该事件的任何计划的执行顺利进行。然而，即使整个系统（包括任何模拟环境）在设计时考虑到了这一点，也总是存在环境是不确定的问题。因此，没有办法保证在+！结束死刑。事实上，这一论证意在表明，在推荐的编程风格中，当事件具有+！它是在一个计划完成执行之后产生的，即使这样，它也不一定被相信（这将在下面第一个引理的证明中考虑有或没有作为一个信念，当打算！然而，只有当程序员明确地包含这样的限制在计划的上下文部分来处理该事件。另一方面，当考虑三对BDI态度中的每一对时，与之相关的是封闭世界假设6，这在Prolog中是众所周知的6有趣的是，(but另一方面，不具体说明如何检查计划上下文是否是信念基础的逻辑结果）。然而，在其最初的定义中，Rao [12]指出，BORDINIAND MOR eIRa118⇒¬¬⇒|⇒⟨⟩/∈<$|⇒⟨⟩|⇒|⇒但也存在于AgentSpeak（L）中。这意味着，对于代理bs，ps，如果bs，则BEL（n）成立。因此，每当在ATP我们有，例如，我们知道，这是一种“以德治国”的行为。因此，根据封闭世界假设，我们可以将AT1重新表述为=意向（）BEL（λ），AT 4 as = INTEND（λ）DES（DES）和AT7as = DES（ε）BEL（ε）。因此，原则AT1、AT4和AT7不能与AgentSpeak（L）（或任何其他使用封闭世界假设的逻辑编程语言）的AT2、AT5和AT8一起被证明。此外，回想一下，一个代理可能会通过感知的信念修正而完全改变其信念基础信念修正函数不是AgentSpeak（L）语义的一部分，而是插入AgentSpeak（L）解释器的一般代理架构的一个组件同样，由于环境是非确定性的，在追求世界的期望或预期状态之后，代理人将相信什么，这一点无法保证引理4.1（AgentSpeak（L）中的意图-信念原则）在AgentSpeak（L）中编程的代理不满足AT 1，但满足AT 2和AT 3。证据考虑到，在任何给定的时间，AgentSpeak（L）agent bs，ps可能会通过其信念修正函数（在这里是一个额外的逻辑过程，因为它不是AgentSpeak（L）语义的一部分）改变其信念集bs，我们不能保证BEL（S）（见定义3.1）在INTEND（S）时为真。因此，AT1不被AgentSpeak（L）代理满足，因此，AT2被满足。反过来，原则AT3也被AgentSpeak（L）代理所满足。公式BEL（BEL-INTEND）（BEL-INTEND）只有当程序员被要求在智能体的计划库中包含所有可能的信念+信念的计划，并且这些计划在其主体中有一个成就目标时！- 是的当然，情况并非如此（从实际编程的角度来看，这是不合理的）。因此，BEL（）INTEND（）无效，因此AT3满足。✷引理4.2（AgentSpeak（L）中的意图-期望原则）在AgentSpeak（L）中编程的代理满足AT 4，不满足AT 5，并且满足AT 6。证据参考定义3.3，我们看到DES（DES）由一个析取定义，INTEND（INTEND）是其中一个析取。很容易看出= INTEND（）DES（），这是AT4的封闭世界版本在那里-因此，AgentSpeak（L）代理满足AT4，当然不满足AT5。AT6原则被AgentSpeak（L）代理所满足，因为，一个AgentSpeak（L）代理的信念基础只有基础信念原子。 这意味着封闭的世界本质上是假定的。Rao非常关心为BDI架构提供一种实际可行的可计算语言。在这方面，他成功了，即使封闭世界假设被证明不适合智能体编程。在证明ATP的最初工作中，为了简单起见，我们保持了最初的定义BORDINIAND MOR eIRa119⟨ ⟩∈⟨ ⟩ ∈∈ ∈⟨⟩ ∈代理人因此，DES（DES）成立，但当没有适用的计划时使用的规则Appl2（见附录）因此，INTEND（INTEND）可能永远不成立，而DES（DES）继续成立。公式INTEND（）只有在应用了Appl1之后才能为真，因此，对于某些i CI或可能稍后的te，i CE（在后一种情况下i是一个暂停的意图），目标（i）：根据定义3.2，这些是INTEND（）成立的条件因此，由于不能保证Appl1将最终应用，因此INTEND（INTEND）可能永远不会保持，即使DES（DES）保持。✷非正式地说，满足AT6表示这样一个事实，即AgentSpeak（L）智能体请注意，在附录中的语义中，我们已经形式化了这样的想法，即如果所选事件在被选中时没有适用的计划，则将其再次包含在事件集中，希望在选择同样，也有可能处理它（参见howCEj在Appl 2中的变化）。另一一种可能性是简单地丢弃事件（两种选择实际上都不是理想的，但这在AgentSpeak（L）文献中没有讨论）。后一种可能性也不会改变AT6的可满足性（INTEND（INTEND）不适用，而DES（DES）适用，即使它仅在被选择和丢弃之前不久适用）。引理4.3（AgentSpeak（L）中的愿望-信念原则）在AgentSpeak（L）中编程的代理不满足AT 7，但满足AT 8和AT 9。证据类似于引理4.1的证明。✷定理4.4（AgentSpeak（L）中的不对称命题原则所有AgentSpeak（L）代理都满足不对称命题原则AT 2、AT 3、AT 4、AT 6、AT 8和AT 9，但做不满足AT1、AT5和AT7。证据 紧接着引理4.1，4.2和4.3。✷推论4.5（等价于BDI逻辑）关于满足的ATP，AgentSpeak（L）不等价于BDI-B1，BDI-B2，BDI-S3，BDI-R3或BDI-W3，如[14]中定义的。证据 Rao和George证明了这些逻辑满足ATP的其他组合;详情参见[14]。✷请注意，Rao和George Rao只分析了ATP的逻辑BDI-B1、BDI-B2、它仍然是调查的其他逻辑在家庭的BDI逻辑，他们在该文件中，以检查是否有任何 满 足 相 同 的 ATP 作 为 AgentSpeak （ L ） 。 这 在 定 义 语 义 上 等 价 于AgentSpeak（L）的逻辑的过程中会很有趣BORDINIAND MOR eIRa1205结论本文为多智能体系统的实现和验证提供了理论支持它介绍了一个框架，证明面向代理的编程语言的BDI属性。然后使用该框架来证明AgentSpeak（L）的ATP根据[14]，AgentSpeak（L）代理满足的ATP的特定组合与一些BDI逻辑满足的ATP组合不未来的工作包括证明AgentSpeak（L）可能满足的其他BDI属性，以及尝试将AgentSpeak（L）与特定的BDI逻辑在它们都满足的BDI属性方面进行匹配。这可能是将AgentSpeak（L）描述为逻辑的第一步，这对于证明（实现的）智能代理的属性很确认这项工作得到了CNPq和FAPERGS的部分支持。第一作者要感谢RobinHirsch（来自UCL-CS），他指出定义一个等价于AgentSpeak（L）的逻辑是很有趣的，以便通过逻辑的常用方法来研究它的属性这项工作并不完全打算这样做，但直接符合（部分灵感来自）这一建议。也非常感谢一位匿名评论者，他的详细评论导致了本文中许多重要问题的讨论引用[1] 博尔迪尼河H、A. L. C.巴赞河O. Jannone，D. M.巴索河M. Vicari和v.R.Lesser，AgentSpeak（XL）：通过决策理论任务调度在BDI代理中进行有效意图选择。Castelfranchi和W.L. Johnson，editors，Proceedings ofthe First International Joint Conference on AutonomousAgents and Multi-Agent Systems（AAMAS-2002，featuring 6th AGENTS，5th ICMAS and9th ATAL） ， 15-19 July， Bologna， Italy（ 2002） ， pp. 公元 1294-1302年。[2] Bratman ， M. E 、 “Intentions, Plans and Practical Reason,” HarvardUniversity Press, Cambridge, MA,[3] deGiacomo ， G. ， Y.Les p'erance 和 H.J.Le vesque ， ConGol og ：Aconcurrent programming language based on the situation calculus，Arti ficialIntelligence 121（2000），pp. 109比169[4] d'Inverno ， M. 和 M. Luck ， Engineering AgentSpeak （ L ） ： A formalcomputational model，Journal of Logic and Computation8（1998），pp. 1-27号。[5] Fisher，M.，并发MetateM语言及其应用的综述，在：D。M. Gabbay和H.J. Ohlbach，编辑，时间逻辑-BORDINIAND MOR eIRa121最小ERVAProceedings of the First International Conference，number 827 in Lecture Notesin Arti Ficial Intelligence，Springer-Verlag，Berlin，1994 pp.480-505[6] George M. P.和A. L. Lansky，Reactive reasoning and planning，in：Proceedings of the Sixth National Conference on Arti Ficial Intelligence（AAAI677-682.[7] Hindriks，K.五、F. S. de Boer，W. van der Hoek和J. J. C. 王文生，王文生，等.基于规则库的智能体语言控制结构的研究. P. Müller，M. P. 辛格和A. S. Rao ， editors ， Intelligent Agents V-Proceedings of the FifthInternational Workshop on Agent Theories，Architectures，and Languages（ATAL-98），held as part of the Agents381-396.[8] Kinny，D.，分布式多智能体推理系统的体系结构和语言规范，技术报告，澳大利亚人工智能研究所，墨尔本，澳大利亚（1993）。[9] 莱特， J.A.， J.J.Alferes 和 L. M. Pereira，-一个动态逻辑 程 序 设 计 代 理 体 系 结 构 ， 在 ： J. - J. Meyer 和 M. Tambe ， editors ，Intelligent Agents VIII -141-157.[10] 马查多河 和R. H. 博迪尼， 运行 AgentSpeak（L） 剂 对 SIM代理，在：J. - J.Meyer和M. 坦比编辑们 智能 Agents VIII -ProceedingsoftheEighthInternational Workshop on Agent Theories，Architectures，andLanguages（ATAL-2001），August1-3，2001，Seattle，WA，number 2333in Lecture Notes in ArtiFicialIntelligence（2002），pp. 158-174。[11] 莫雷拉，A'。F. 和R. H. Bordini，BDI的非面向代理的编程语言，在：Proceedings of the Workshop on Logics for Agent-Based Systems（LABS-02），held in conjunction with the Eighth InternationalConference on Principles of Knowledge Representation and Reasoning （ KR2002），April 2245比59[12] Rao，A.美国，AgentSpeak（L）：BDI代理以逻辑可计算语言说话，在：W。Van de Velde和J.Perram，编辑，第七届多智能体世界中的自主智能体建模研讨会论文集（MAAMAW42比55[13] Rao，A.S. 和M.P. 乔治·巴茨，BDI代理人：从理论到实践，在：V。Lesser 和 L.Gasser ， editors ， Proceedings of the First InternationalConference on Multi-Agent Systems（ICMAS312-319.[14] Rao，A. S.和M. P. George P.，Decision procedures for BDI logics，Journalof Logic and Computation8（1998），pp. 293-343BORDINIAND MOR eIRa122[15] Shoham，Y.，面向Agent的编程，人工智能60（1993），pp。51比92[16] 辛格，M。P.，A. S. Rao和M.陈文辉，“基于逻辑的DAI形式化方法与推理”，载于：Weigeant，编辑，Multiagent Systems-A Modern Approach toDistributed Arti Ficial Intelligence，麻省理工学院出版社，剑桥，MA，1999页。331-376.[17] Sloman，A. 和B. 洛根，建筑认知丰富 剂 使用 SIM代理工具包，计算机械协会通信43（1999），pp. 71比77[18] Winiko M.，L. Padgham，J.Harland和J.Thangarajah，智能代理系统中的声明性和程序性目标，在：第八届知识表示和推理原则国际会议（KR2002），4月22日470-481.BORDINIAND MOR eIRa123≥⟨⟩AgentSpeak（L）的一种表示和这 是 在 [11] 中 给 出 的 AgentSpeak（L）的语法和语义。这里以一种非常简洁的方式提出;请参阅该论文的评论介绍。为了允许更紧凑的表示，关于推理规则的附带条件被显示在它们下面，前面有语法• AgentSpeak（L）代理ag：：=bs psbs：：= b1. bn（n≥ 0）PS * = p1. pn（n≥ 1）• 信仰at：：=P（t1，...， tn）（n0）其中P是谓词符号;信念是没有变量的原子(we使用b表示信念）• 计划p：：=te：ct<-hte 触发事件ct上下文h行动、目标和信念更新的顺序（计划• 上下文ct：：=at | ¬at | ct ∧ ct |T• 行动，目标，信念更新，计划主体a的范围超过基本动作g：：=！在|什么？在u：：= + b|−bh：：= a|G |u|h; h· ！at是一个成就目标· ？at是测