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

本文迈出了从实验中学习的逻辑的第一步。为此，我们调查了建模因果和（定性）认知推理的相互作用的正式框架。对于我们的方法至关重要是一种干预概念的想法，可以用作（真实或假设的）实验的正式表达。在第一步中，我们将众所周知的因果模型与代理人的认知状态的简单HITIKKA样式表示。在生成的设置中，不仅可以对关于变量值的知识以及干预措施如何影响它们，而且可以对其进行交谈，而且还可以谈论知识更新。由此产生的逻辑可以模拟关于思想实验的推理。但是，它无法解释从实验中学习，这显然是由它验证干预措施没有学习原则的事实。因此，在第二步中，我们实现更复杂的知识概念，该知识概念允许代理在进行实验时观察（测量）某些变量。该扩展系统确实允许从实验中学习。对于所有提出的逻辑系统，我们提供了一种声音和完整的公理化。

A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a pairwise message exchange (telephone call) wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition is that all agents are experts. Instead, we explore protocols wherein the termination condition is that all agents know that all agents are experts. We call such agents super experts. We also investigate gossip protocols that are common knowledge among the agents. Additionally, we model that agents who are super experts do not make and do not answer calls, and that this is common knowledge. We investigate conditions under which protocols terminate, both in the synchronous case, where there is a global clock, and in the asynchronous case, where there is not. We show that a commonly known protocol with engaged agents may terminate faster than the same commonly known protocol without engaged agents.

Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in `it is common knowledge among economists'. We introduce such a logic of common knowledge, which we term abstract-group epistemic logic (AGEL). That is, AGEL features a common knowledge operator for groups of agents given by concepts in a separate agent logic that we keep generic, with one possible agent logic being ALC. We show that AGEL is EXPTIME-complete, with the lower bound established by reduction from standard group epistemic logic, and the upper bound by a satisfiability-preserving embedding into the full $\mu$-calculus. Further main results include a finite model property (not enjoyed by the full $\mu$-calculus) and a complete axiomatization.

我们概述了在其知识表示和声明问题解决的应用中的视角下的时间逻辑编程。这些程序是将通常规则与时间模态运算符组合的结果，如线性时间时间逻辑（LTL）。我们专注于最近的非单调形式主义的结果​​称为时间平衡逻辑（电话），该逻辑（电话）为LTL的全语法定义，但是基于平衡逻辑执行模型选择标准，答案集编程的众所周知的逻辑表征（ASP ）。我们获得了稳定模型语义的适当延伸，以进行任意时间公式的一般情况。我们记得电话和单调基础的基本定义，这里的时间逻辑 - 和那里（THT），并研究无限和有限迹线之间的差异。我们还提供其他有用的结果，例如将转换成其他形式主义，如量化的平衡逻辑或二阶LTL，以及用于基于自动机计算的时间稳定模型的一些技术。在第二部分中，我们专注于实际方面，定义称为较近ASP的时间逻辑程序的句法片段，并解释如何在求解器Telingo的构建中被利用。

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

In dynamic epistemic logic (Van Ditmarsch et al., 2008) it is customary to use an action model (Baltag and Moss, 2004; Baltag et al., 1998) to describe different views of a single action. In this article, action models are extended to add or remove agents, we call these agent-update models. This can be done selectively so that only some specified agents get information of the update, which can be used to model several interesting examples such as private update and deception, studied earlier by Baltag and Moss (2004); Sakama (2015); Van Ditmarsch et al. (2012). The product update of a Kripke model by an action model is an abbreviated way of describing the transformed Kripke model which is the result of performing the action. This is extended to a sum-product update of a Kripke model by an agent-update model in the new setting. We show that dynamic doxastic logic with action modalities, now based on agent-update models, continues to have a sound and complete proof system. We have simple decision procedures for model checking and validity.

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

知识可定义是合理的真实信念（“JTB”）？我们认为，人们可以积极地或负面地回答，具体取决于一个人的真实信仰是否合理，我们称之为足够的原因。为了促进我们的论点，我们介绍了一个简单的基于理性的信念的命题逻辑，并提出了充分性的概念的公理表征。我们表明，此逻辑足以灵活，以适应各种有用的功能，包括由于原因的量化。我们使用我们的框架对比JTB的两位概念进行对比：一个内部家，另一家族。我们认为Gettier案例基本上挑战了内部概念，但不是外科医生。我们的方法致力于一系列关于知识的非押金主义，但它也让我们陷入困境，即知识是否涉及只有足够的原因，或者留下房间的原因不足。我们赞成后者的立场，这反映了一个更温和和更现实的无押金主义。

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.

形状约束语言（SHACL）是通过验证图表上的某些形状来验证RDF数据的最新W3C推荐语言。先前的工作主要集中在验证问题上，并且仅针对SHACL的简化版本研究了对设计和优化目的至关重要的可满足性和遏制的标准决策问题。此外，SHACL规范不能定义递归定义的约束的语义，这导致文献中提出了几种替代性递归语义。尚未研究这些不同语义与重要决策问题之间的相互作用。在本文中，我们通过向新的一阶语言（称为SCL）的翻译提供了对SHACL的不同特征的全面研究，该语言精确地捕获了SHACL的语义。我们还提出了MSCL，这是SCL的二阶扩展，它使我们能够在单个形式的逻辑框架中定义SHACL的主要递归语义。在这种语言中，我们还提供了对过滤器约束的有效处理，这些滤镜经常在相关文献中被忽略。使用此逻辑，我们为不同的SHACL片段的可满足性和遏制决策问题提供了（联合）可决定性和复杂性结果的详细图。值得注意的是，我们证明这两个问题对于完整的语言都是不可避免的，但是即使面对递归，我们也提供了有趣的功能的可决定性组合。

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

在概念学习，数据库查询的反向工程，生成参考表达式以及知识图中的实体比较之类的应用中，找到以标记数据项形式分开的逻辑公式，该公式分开以标记数据项形式给出的正面和负面示例。在本文中，我们研究了存在本体论的数据的分离公式的存在。对于本体语言和分离语言，我们都专注于一阶逻辑及其以下重要片段：描述逻辑$ \ Mathcal {alci} $，受保护的片段，两变量的片段和受保护的否定片段。为了分离，我们还考虑（工会）连接性查询。我们考虑了几种可分离性，这些可分离性在负面示例的治疗中有所不同，以及他们是否承认使用其他辅助符号来实现分离。我们的主要结果是（所有变体）可分离性，不同语言的分离能力的比较以及确定可分离性的计算复杂性的研究。

它在智能代理系统中起着核心作用，以模拟代理的认知状态及其变化。为此，已经提出了一些正式系统。其中，认知逻辑侧重于不同认知属性（例如知识，信仰，常识等）和认知行动（例如，公开公告，私人公告，异步公告等）的逻辑定律。所有这些系统都不涉及代理与其环境之间的交互行为。通过丰富众所周知的$ \ pi $ -calculus，本文介绍了电子库，该论文提供了一个概念框架，以模拟代理人与认知状态的认知相互作用。与通常的过程演算不同，始终安排电子库中的所有系统以在认知状态下运行。为了抽象地形式化认知状态，提出了一群假设。此外，基于这些假设，电子钙的行为理论是在两个不同的观点中开发的。

近年来，人们对布尔功能的重新兴趣在解释可解释的AI（XAI）领域的二元分类器方面产生了兴趣。布尔函数的标准方法是命题逻辑。我们提出了一种ceteris paribus性质的模态语言，该语言支持有关二进制输入分类器及其属性的推理。我们研究一个分类器模型家庭，将其作为有关语言基础性的两个证明系统，并显示出我们的Axiomatics的完整性。此外，我们证明，我们模态语言的可满足性检查问题在无限变化的情况下是nexptime-complete，而在有限变量的情况下它变为多项式。在无限变化的情况下，我们还确定了我们语言的有趣的NP片段。我们利用语言来形式化反事实的条件以及各种解释概念，包括绑架，对比和反事实解释以及偏见。最后，我们介绍了我们的语言的两个扩展：通过分配的概念使分类器变化和认知扩展，可以表示分类器对实际输入的不确定性。

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

忘记 - 或可变消除 - 是一种允许从知识库中删除中间变量的操作，不再被视为相关。近年来，已经提出了许多忘记答案编程的不同方法，以特定运营商或这些运营商的类别，通常遵循不同的原则并遵守不同的性质。开发了每个这样的方法，以解决忘记某些特定的观点，旨在遵守在这种观点中认为所希望的特定属性，但缺少所有现有运营商和属性的全面和统一概述。在本文中，我们彻底检查了现有的属性和（类别的）运营商忘记了答案集编程，绘制了这些遗忘运营商的景观的完整图片，其中包括许多新颖的属性和运营商之间关系的结果，包括考虑因素在混凝土运营商上，计算遗忘和计算复杂性的结果。我们的目标是提供指导，帮助用户选择运营商最适合其应用要求。

本文建立了关于知识和论证的双重理论。我们的思想既植根于认知逻辑和论证理论，我们的目标是以浅表的方式合并这两个领域，而且还彻底披露了知识和论证之间的内在相关性。具体而言，我们将认知的Kripke模型和参数Kripke模型定义为双对，然后在这两种类型的Kripke模型之间制定了双向生成方法。这一代是通过对模态公式的不变性的双重定理的严格合理的。我们还提供了现实的例子来展示我们这一代人，通过这些示例，我们的框架的实用性得到了强有力的提倡。我们最终提出了一个哲学论文，即知识本质上是动态的，我们与麦克斯韦的恶魔以及众所周知的谚语“知识就是力量”建立了一定的联系。

我们回答以下问题，哪些结合性查询以多种方式上的许多正和负面示例以及如何有效地构建此类示例的特征。结果，我们为一类连接的查询获得了一种新的有效的精确学习算法。我们的贡献的核心是两种新的多项式时间算法，用于在有限结构的同态晶格中构建前沿。我们还讨论了模式映射和描述逻辑概念的独特特征性和可学习性的影响。

对指示性有条件的研究通常旨在确定其真实条件，或者解释我们应该如何与他们进行推理以及何时可以主张它们。本文通过阐明指示性有条件的三价，真实功能的真理条件来整合这些语义和认识论项目。基于此框架，我们提供了有条件概率的非经典说明，以及有条件推理的两个逻辑：（i）从某些前提中推断的逻辑C，可以推断推断推理；（ii）从不确定前提中推断的逻辑U，概括了不诚实的推理。两种逻辑在其领域都非常有吸引力。它们为有条件推理提供了一个统一的框架，概括了现有理论（例如，亚当斯的“合理推论”逻辑），并对有关Modus Ponens，Import-Export和其他条件逻辑原理的争议进行了深入的分析。