Over the recent twenty years, argumentation has received considerable attention in the fields of knowledge representation, reasoning, and multi-agent systems. However, argumentation in dynamic multi-agent systems encounters the problem of significant arguments generated by agents, which comes at the expense of representational complexity and computational cost. In this work, we aim to investigate the notion of abstraction from the model-checking perspective, where several arguments are trying to defend the same position from various points of view, thereby reducing the size of the argumentation framework whilst preserving the semantic flow structure in the system.

This volume contains revised versions of the papers selected for the third volume of the Online Handbook of Argumentation for AI (OHAAI). Previously, formal theories of argument and argument interaction have been proposed and studied, and this has led to the more recent study of computational models of argument. Argumentation, as a field within artificial intelligence (AI), is highly relevant for researchers interested in symbolic representations of knowledge and defeasible reasoning. The purpose of this handbook is to provide an open access and curated anthology for the argumentation research community. OHAAI is designed to serve as a research hub to keep track of the latest and upcoming PhD-driven research on the theory and application of argumentation in all areas related to AI.

一个自治系统由制造商构建，在患有规范和法律的社会中运营，并与最终用户进行互动。所有这些行动者都是受自治系统行为影响的利益相关者。我们解决这些利益攸关方的道德观点的挑战可以集成在自治系统的行为中。我们提出了一个道德推荐组件，我们称之为JIMINY，它使用规范系统和正式论证的技术，以达到利益攸关方之间的道德协议。 JIMINY代表了使用规范系统的每个利益相关者的道德观点，并有三种解决涉及利益攸关方意见的道德困境。首先，JIMINY认为利益相关者的论据是如何彼此相关的，这可能已经解决了困境。其次，JIMINY结合了利益攸关方的规范性系统，使利益攸关方的合并专业知识可能解决困境。第三，只有当这两种其他方法失败时，JIMINY使用上下文敏感的规则来决定哪个利益相关者优先考虑。在抽象层面，这三种方法的特点是添加参数，参数之间的攻击以及争论之间的攻击。我们展示了JIMINY不仅可以用于道德推理和协作决策，而且还用于提供关于道德行为的解释。

基于领域的模型计划者通常通过通过放松或抽象的符号世界模型来构建搜索启发式方法来得出他们的普遍性。我们说明抽象解释如何作为这些基于抽象的启发式方法的统一框架，将启发式搜索的范围扩展到更丰富的世界模型，这些模型利用更复杂的数据类型和功能（例如集合，几何形状），甚至具有不确定性和不确定性和不确定性和模型概率效应。这些启发式方法也可以与学习相结合，从而使代理可以通过抽象衍生的信息在新颖的世界模型中开始计划，这些信息随后通过经验来完善。这表明抽象的解释可以在构建通用推理系统中起关键作用。

机器人操作系统（ROS）是用于构建机器人系统的广泛使用的框架。它提供了各种可重复使用的软件包和新开发项目的模式。开发人员如何将这些元素结合在一起，并将它们与自主行为的决策集成在一起。总体上最有价值的决策的特征是安全保证。在本研究预览中，我们提出了一种正式的方法，可以在ROS中产生安全的自主决策。我们首先描述了如何改善现有的静态验证方法，以验证多目标多代理决策。之后，我们描述了如何从改进的静态验证方法过渡到提出的运行时验证方法。该研究提案的初步实施得出了有希望的结果。

机器人系统的长期自主权隐含地需要可靠的平台，这些平台能够自然处理硬件和软件故障，行为问题或缺乏知识。基于模型的可靠平台还需要在系统开发过程中应用严格的方法，包括使用正确的构造技术来实现机器人行为。随着机器人的自治水平的提高，提供系统可靠性的提供成本也会增加。我们认为，自主机器人的可靠性可靠性可以从几种认知功能，知识处理，推理和元评估的正式模型中受益。在这里，我们为自动机器人代理的认知体系结构的生成模型提出了案例，该模型订阅了基于模型的工程和可靠性，自主计算和知识支持机器人技术的原则。

AI的蓬勃发展提示建议，AI技术应该是“以人为本”。然而，没有明确的定义，对人工人工智能或短，HCAI的含义。本文旨在通过解决HCAI的一些基础方面来改善这种情况。为此，我们介绍了术语HCAI代理商，以指配备有AI组件的任何物理或软件计算代理，并与人类交互和/或协作。本文识别参与HCAI代理的五个主要概念组件：观察，要求，行动，解释和模型。我们看到HCAI代理的概念，以及其组件和功能，作为弥合人以人为本的AI技术和非技术讨论的一种方式。在本文中，我们专注于采用在人类存在的动态环境中运行的单一代理的情况分析。

即将开发我们呼叫所体现的系统的新一代越来越自主和自学习系统。在将这些系统部署到真实上下文中，我们面临各种工程挑战，因为它以有益的方式协调所体现的系统的行为至关重要，确保他们与我们以人为本的社会价值观的兼容性，并且设计可验证安全可靠的人类-Machine互动。我们正在争辩说，引发系统工程将来自嵌入到体现系统的温室，并确保动态联合的可信度，这种情况意识到的情境意识，意图，探索，探险，不断发展，主要是不可预测的，越来越自主的体现系统在不确定，复杂和不可预测的现实世界环境中。我们还识别了许多迫切性的系统挑战，包括可信赖的体现系统，包括强大而人为的AI，认知架构，不确定性量化，值得信赖的自融化以及持续的分析和保证。

本文介绍了逻辑代理的运行时间自检的全面框架，通过时间公理进行动态检查。通过使用定义为此目的的代理导向的间隔时间逻辑来指定这些公理。我们为此新逻辑定义了语法，语义和语用，专门针对代理的应用程序定制。在由此产生的框架中，我们包括并扩展过去的工作。

本文使用JACAMO框架提供了多代理系统（MAS）的运行时验证（RV）方法。我们的目标是为MAS带来一层安全性。该层能够在系统执行过程中控制事件，而无需在每个代理的行为中进行特定的实现来识别事件。MAS已在混合智能的背景下使用。这种使用需要软件代理与人类之间的通信。在某些情况下，通过自然语言对话进行沟通。但是，这种沟通使我们引起了与控制对话流有关的关注，因此代理可以防止讨论主题的任何变化可能会损害其推理。我们证明了一个监视器的实施，该监视器旨在控制MAS中的对话流，该对话流通过自然语言与用户沟通以帮助医院病床分配的决策。

The standard semantics of multi-agent epistemic logic S5 is based on Kripke models whose accessibility relations are reflexive, symmetric and transitive. This one dimensional structure contains implicit higher-dimensional information beyond pairwise interactions, that we formalized as pure simplicial models in a previous work (Information and Computation, 2021). Here we extend the theory to encompass simplicial models that are not necessarily pure. The corresponding class of Kripke models are those where the accessibility relation is symmetric and transitive, but might not be reflexive. Such models correspond to the epistemic logic KB4 . Impure simplicial models arise in situations where two possible worlds may not have the same set of agents. We illustrate it with distributed computing examples of synchronous systems where processes may crash.

在过去几年的几十年中，致力于更新稳定模型语义（AKA答案设置程序）下更新逻辑计划的问题，或者换句话说，表现出培养结果的问题 - 当它描述更改时，遵守逻辑程序。而最先进的方法是在古典逻辑背景下的相同基本的直觉和愿望被指导，他们基于根本不同的原则和方法，这阻止了可以拥抱两个信念的统一框架规则更新。在本文中，我们将概述与答案设置的编程更新相关的一些主要方法和结果，同时指出本主题研究的一些主要挑战。

已经开发了概率模型检查，用于验证具有随机和非季度行为的验证系统。鉴于概率系统，概率模型检查器占用属性并检查该系统中的属性是否保持。因此，概率模型检查提供严谨的保证。然而，到目前为止，概率模型检查专注于所谓的模型，其中一个状态由符号表示。另一方面，通常需要在规划和强化学习中进行关系抽象。各种框架处理关系域，例如条带规划和关系马尔可夫决策过程。使用命题模型检查关系设置需要一个地接地模型，这导致了众所周知的状态爆炸问题和难以承承性。我们提出了PCTL-Rebel，一种用于验证关系MDP的PCTL属性的提升模型检查方法。它延长了基于关系模型的强化学习技术的反叛者，朝着关系PCTL模型检查。 PCTL-REBEL被提升，这意味着而不是接地，模型利用对称在关系层面上整体的一组对象。从理论上讲，我们表明PCTL模型检查对于具有可能无限域的关系MDP可判定，条件是该状态具有有界大小。实际上，我们提供算法和提升关系模型检查的实现，并且我们表明提升方法提高了模型检查方法的可扩展性。

本文对法律合同签署的流程产生了逻辑理解，其申请在区间平台上的智能合同的法律承认智能合同的基础上。开发了许多公理和推论规则，可以用于证明从某些内容签署的事实中为合同形成的“思想会议”的前提。除了“提供和验收”的过程之外，该文件还考虑了同行的“签名”，这是一个独立的双方或可能，远程）签署合同的不同副本，而不是将他们的签名放在常见的副本上。有人认为，对应于同行的签名令人满意的签名与句法自我引用的逻辑。使用的公理由正式的语义支持，并研究了逻辑的一些进一步性质。特别是，表明逻辑意味着当合同已签署时，各方不仅仅是一致，而且是关于合同条款的相互协议（一个共同知识的概念）。

General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent generations quickly. What structure enables this, and how might that inform automated mathematical reasoning? We posit that central to both puzzles is the structure of procedural abstractions underlying mathematics. We explore this idea in a case study on 5 sections of beginning algebra on the Khan Academy platform. To define a computational foundation, we introduce Peano, a theorem-proving environment where the set of valid actions at any point is finite. We use Peano to formalize introductory algebra problems and axioms, obtaining well-defined search problems. We observe existing reinforcement learning methods for symbolic reasoning to be insufficient to solve harder problems. Adding the ability to induce reusable abstractions ("tactics") from its own solutions allows an agent to make steady progress, solving all problems. Furthermore, these abstractions induce an order to the problems, seen at random during training. The recovered order has significant agreement with the expert-designed Khan Academy curriculum, and second-generation agents trained on the recovered curriculum learn significantly faster. These results illustrate the synergistic role of abstractions and curricula in the cultural transmission of mathematics.

We are currently unable to specify human goals and societal values in a way that reliably directs AI behavior. Law-making and legal interpretation form a computational engine that converts opaque human values into legible directives. "Law Informs Code" is the research agenda capturing complex computational legal processes, and embedding them in AI. Similar to how parties to a legal contract cannot foresee every potential contingency of their future relationship, and legislators cannot predict all the circumstances under which their proposed bills will be applied, we cannot ex ante specify rules that provably direct good AI behavior. Legal theory and practice have developed arrays of tools to address these specification problems. For instance, legal standards allow humans to develop shared understandings and adapt them to novel situations. In contrast to more prosaic uses of the law (e.g., as a deterrent of bad behavior through the threat of sanction), leveraged as an expression of how humans communicate their goals, and what society values, Law Informs Code. We describe how data generated by legal processes (methods of law-making, statutory interpretation, contract drafting, applications of legal standards, legal reasoning, etc.) can facilitate the robust specification of inherently vague human goals. This increases human-AI alignment and the local usefulness of AI. Toward society-AI alignment, we present a framework for understanding law as the applied philosophy of multi-agent alignment. Although law is partly a reflection of historically contingent political power - and thus not a perfect aggregation of citizen preferences - if properly parsed, its distillation offers the most legitimate computational comprehension of societal values available. If law eventually informs powerful AI, engaging in the deliberative political process to improve law takes on even more meaning.

提出了具有依赖常识的公共公告逻辑的浅语义嵌入。此嵌入使得该逻辑的首次自动化为经典高阶逻辑的现成定理传输。据证明（i）可以通过这种方式自动化的荟萃理论研究，（ii）所需的目标逻辑（公共公告逻辑）的非琐碎推理方式是如何实现的。为了获得令人信服的编码和智者自动化，可以实现。呈现的语义嵌入的关键是评估域在嵌入目标逻辑的组成部分的编码中被明确建模并视为附加参数;在以前的相关工程中，例如在嵌入正常模态逻辑中，在元逻辑和目标逻辑之间隐式共享评估域。本文所呈现的工作构成了对多元日志知识工程方法的重要补充，这使得能够通过逻辑及其组合进行实验，以及一般和域知识，以及混凝土用例 - 同时。

确保未来变革性人工智能（TAI）或人工高智（ASI）系统的安全性存在几种不同的方法，以及不同方法的支持者对其在近期工作的重要性或有用性具有不同和辩论的索赔，以及未来的系统。高度可靠的代理设计（HRAD）是由机器智能研究所等领域的最具争议和雄心勃勃的方法之一，其中包括各种论点以及如何减少未来AI系统的风险。为了减少关于AI安全的辩论中的困惑，在这里，我们在米饭上建立了以前的讨论，该米饭收集并提出了四个中央论点，这些论点用于证明HRAD作为AI系统安全的路径。我们签下了争论（1）附带效用，（2）碎片灌注，（3）精确规范，（4）预测。这些中的每一个都具有不同的，部分冲突的索赔关于未来AI系统可能是风险的。我们已经根据发布和非正式文献的审查，并与对该主题职位的专家进行磋商，解释了假设和索赔。最后，我们简要概述了针对每种方法和整体议程的论据。

我们提出了五个基本的认知科学基本宗旨，我们在相关文献中认真地将其确定为该哲学的主要基本原则。然后，我们开发一个数学框架来讨论符合这些颁布宗旨的认知系统（人造和自然）。特别是我们注意，我们的数学建模并不将内容符号表示形式归因于代理商，并且代理商的大脑，身体和环境的建模方式使它们成为更大整体的不可分割的一部分。目的是为认知创造数学基础，该基础符合颁布主义。我们看到这样做的两个主要好处：（1）它使计算机科学家，AI研究人员，机器人主义者，认知科学家和心理学家更容易获得颁发的思想，并且（2）它为哲学家提供了一种可以使用的数学工具，可以使用它澄清他们的观念并帮助他们的辩论。我们的主要概念是一种感觉运动系统，这是过渡系统研究概念的特殊情况。我们还考虑了相关的概念，例如标记的过渡系统和确定性自动机。我们分析了一个名为“足够的概念”，并表明它是“从颁布主义的角度来看”中“认知数学数学”中基础概念的一个很好的候选者。我们通过证明对最小的完善（在某种意义上与生物体对环境的最佳调整相对应）的独特定理来证明其重要性，并证明充分性与已知的概念相对应，例如足够的历史信息空间。然后，我们开发其他相关概念，例如不足程度，普遍覆盖，等级制度，战略充足。最后，我们将其全部绑架到颁布的宗旨。

在这项调查中，我们回顾了动态认知逻辑，具有量化信息变化的方式。在此类逻辑中，我们提出了完整的公理化，重点关注涉及知识与此类量化器之间相互作用的公理，我们报告了它们的相对表现，可定义性以及模型检查和满意度的复杂性以及应用程序的复杂性。我们专注于开放问题和新的研究方向。