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

我们从答案集编程的民间传说中占据了一个想法，即选择，完整性约束以及限制规则格式足以回答集编程。我们在这里的逻辑的背景下详细说明了这个想法的基础，并展示了如何通过定义从扩展的逻辑原则派生。然后，我们提供了一种AUSTERE形式的逻辑程序，可以用作类似于古典逻辑中的联合常规表的逻辑程序的正常形态。最后，我们采取关键的想法，并为ASP初学者提出建模方法，并说明如何使用它。

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

回答集编程（ASP）已成为一种流行的和相当复杂的声明问题解决方法。这是由于其具有吸引力的地址解决方案的工作流程，这是可以轻松解决问题解决的方法，即使对于计算机科学外的守护者而言。与此不同，底层技术的高度复杂性使得ASP专家越来越难以将想法付诸实践。有关解决此问题，本教程旨在使用户能够构建自己的基于ASP的系统。更确切地说，我们展示了ASP系统Clingo如何用于扩展ASP和实现定制的专用系统。为此，我们提出了两个替代方案。我们从传统的AI技术开始，并展示元编程如何用于扩展ASP。这是一种相当轻的方法，依赖于Clingo的reation特征来使用ASP本身表达新功能。与此不同，本教程的主要部分使用传统的编程（在Python中）来通过其应用程序编程接口操纵Clingo。这种方法允许改变和控制ASP的整个模型 - 地面解决工作流程。 COMENT of Clingo的新应用程序课程使我们能够通过自定义类似于Clingo中的进程来绘制Clingo的基础架构。例如，我们可能会互动到程序的抽象语法树，控制各种形式的多射击求解，并为外国推论设置理论传播者。另一种横截面结构，跨越元以及应用程序编程是Clingo的中间格式，即指定底层接地器和求解器之间的界面。我们通过示例和几个非琐碎的案例研究说明了本教程的前述概念和技术。

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

我们在答案集编程（ASP）中，提供了全面的可变实例化或接地的理论基础。在ASP的建模语言的语义上构建，我们在（固定点）运营商方面介绍了接地算法的正式表征。专用良好的运营商扮演了一个主要作用，其相关模型提供了划定接地结果以及随机简化的语义指导。我们地址呈现出一种竞技级逻辑程序，该程序包含递归聚合，从而达到现有ASP建模语言的范围。这伴随着一个普通算法框架，详细说明递归聚集体的接地。给定的算法基本上对应于ASP接地器Gringo中使用的算法。

线性时间逻辑（LTL）是最受欢迎的时间逻辑之一，它在计算机科学的各种分支中发挥作用。在其广泛使用的各种原因中，它具有强大的基础特性：LTL等于无反欧米茄 - 自动疗法，与无星的欧米茄表达式，以及（通过Kamp的定理）与一个继任者的一阶理论（S1S [FO]）。安全性和共同安全性语言，其中有限的前缀足以确定单词是否不属于或属于该语言，在降低LTL的模型检查和反应性合成等问题的复杂性方面起着至关重要的作用。 safetyltl（分别，cosafetyltl）是LTL的片段，其中只允许通用（分别，存在的）时间方式，仅识别安全性（分别，共同安全）语言。本文的主要贡献是引入了S1S [FO]的片段，称为Safetyfo及其双Cosafetyfo，它们在LTL可定义的安全性和共同安全性语言方面表现出色。我们证明它们分别表征了Safetyltl和Cosafetyltl，这是加入Kamp定理的结果，并更清晰地看出了（片段）LTL的（片段）在一阶语言方面。此外，它提供了直接，紧凑且独立的证据，表明LTL中可以定义的任何安全语言在Safetyltl中也可以定义。作为副产品，我们获得了Safetyltl弱明天运营商的表达能力的一些有趣结果，该实力对有限和无限单词进行了解释。此外，我们证明，当用有限的单词解释时，Safetyltl（cosafetyltl）没有明天（分别，弱的明天）操作员捕获了LTL的安全性（分别，共同安全）片段，而不是有限词。

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

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

本文继续进行研究旨在研究逻辑程序与一阶理论之间的关系。我们将程序完成的定义扩展到具有输入和输出的程序的定义，以ASP接地器Gringo的输入语言的子集，研究稳定模型与在此背景下完成之间的关系，并使用两种软件工具（使用两个软件工具）来描述初步实验国歌和吸血鬼，以验证输入和输出的程序的正确性。定理的证明是基于将本文研究的程序语义与稳定模型的一阶公式模型相关联的引理。在TPLP中接受的考虑。

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

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

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

模态逻辑的语言能够在Kripke帧上表达一阶条件。 Henrik Sahlqvist的经典结果确定了一类重要的模态公式，可以以有效的算法方式找到一阶条件（或Sahlqvist通讯）的一阶条件（或Sahlqvist通讯）。最近的作品已成功将这种经典结果扩展到更复杂的模态语言。在本文中，我们追求类似的行并为线性时间逻辑（LTL）开发SAHLQVIST式通讯定理，该定理是用于时间规范的最广泛使用的正式语言之一。 LTL使用专用的临时操作员下一个X和直到U扩展了基本模态逻辑的语法。结果，具有一阶通讯器的公式类别的复杂性也相应增加。在本文中，我们确定了使用模态运算符F，G，X和U构建的一类重要的LTL SAHLQVIST公式。本文的主要结果是证明LTL SAHLQVIST公式对框架条件的对应关系，这些条件在一阶语言中可定义。

Two approaches to AI, neural networks and symbolic systems, have been proven very successful for an array of AI problems. However, neither has been able to achieve the general reasoning ability required for human-like intelligence. It has been argued that this is due to inherent weaknesses in each approach. Luckily, these weaknesses appear to be complementary, with symbolic systems being adept at the kinds of things neural networks have trouble with and vice-versa. The field of neural-symbolic AI attempts to exploit this asymmetry by combining neural networks and symbolic AI into integrated systems. Often this has been done by encoding symbolic knowledge into neural networks. Unfortunately, although many different methods for this have been proposed, there is no common definition of an encoding to compare them. We seek to rectify this problem by introducing a semantic framework for neural-symbolic AI, which is then shown to be general enough to account for a large family of neural-symbolic systems. We provide a number of examples and proofs of the application of the framework to the neural encoding of various forms of knowledge representation and neural network. These, at first sight disparate approaches, are all shown to fall within the framework's formal definition of what we call semantic encoding for neural-symbolic AI.

在科学和工程领域中，搜索优化问题是很多。长期以来，人工智能为搜索算法和旨在解决和建模搜索优化问题的宣言编程语言的发展做出了贡献。自动推理和知识表示是AI的子场，这些子场尤其归属这些发展。许多流行的自动推理范式为用户提供支持优化语句的语言。召回整数线性编程，MAXSAT，优化满意度模型理论和（约束）答案集编程。这些范式在其语言上以它们在计算解决方案上表达质量条件的方式差异很大。在这里，我们提出了一个所谓的扩展权重系统的统一框架，以消除范式之间的句法区别。它们使我们能够看到不同自动推理语言提供的优化语句之间的基本相似性和差异。我们还研究了提议的系统的形式属性，这些系统立即转化为可以在我们的框架内捕获的范式的形式属性。在逻辑编程（TPLP）的理论和实践中考虑的考虑因素。

ALChour \“Ardenfors的AGM发布，Makinson继续代表与信仰变革有关的研究中的基石。Katsuno和Mendelzon（K＆M）通过了AGM假设改变信仰基地，并在命题中的特征agm信仰基地修订有限签名的逻辑。我们概括了K＆M在任意Tarskian逻辑中设置的（多个）基本修订版的方法，涵盖了具有经典模型 - 理论语义的所有逻辑，从而涵盖了知识表示和超越的各种逻辑。我们的通用配方适用于“基础”的各种概念（例如信仰集，任意或有限的句子或单句话）。核心结果是表示AGM基本修订运算符和某些“分配”之间双向对应的表示定理：函数映射信仰基础到总数 - 尚未传递 - “偏好”解释之间的关系。与此同时，我们为CAS提供了一个伴侣E当agm andodatience的AGM假设被遗弃时。我们还提供了所有逻辑的表征，我们的结果可以加强生产传递偏好关系的分配（如K＆M的原始工作），根据语法依赖与独立性，引起了这种逻辑的两个表示定理。

突出非克劳兰（NC）公式的富有表现性比基于氏子型公式的指数更丰富。然而，氏菌效率优于非克劳尿的效率。实际上，后者的一个主要弱点是，虽然喇叭子宫公式以及喇叭算法，对于高效率至关重要，但是已经提出了非符号形式的喇叭状公式。为了克服这种弱点，我们通过将喇叭图案充分提升到NC形式，定义HOLE非字母（HORN-NC）公式的混合类$ \ MATHBB {H_ {NC}}。争论$ \ MATHBB {H_ {NC}} $以及未来的Horn-NC算法，应随着喇叭类的股份效率增加，增加非信用效率。其次，我们：（i）给出$ \ mathbb的紧凑，归纳定义{h_ {nc}} $; （ii）证明了句法$ \ mathbb {h_ {nc}} $ suppups over class，但语义上两个类都是等效的，并且（iii）表征属于$ \ mathbb {h_ {nc}} $的非锁友公式。第三，我们定义了非字词单元分辨率计算，$ ur_ {nc} $，并证明它检查多项式时间$ \ mathbb {h_ {nc}} $的可靠性。这一事实是我们的知识，使$ \ mathbb {h_ {nc}} $中的nc推理中的第一个特征多项式类。最后，我们证明了$ \ mathbb {h_ {nc}} $线性识别，也是严格的是法官和比喇叭类呈指数富裕。我们在NC自动推理中讨论了这一点，例如，可靠性解决，定理证明，逻辑编程等可以直接受益于$ \ mathbb {h_ {nc} $和$ ur_ {nc} $，它作为其被证明属性的副产物，$ \ mathbb { H_ {NC}} $ as作为分析喇叭函数和含义系统的新替代方案。

混合MKNF的逻辑（最少的知识和否定为失败）是一种强大的知识表示语言，它优雅地将ASP（答案集编程）与本体结合在一起。析取规则是基于正常规则的推理的理想扩展，通常是为正常知识基础设计的语义框架，需要进行大量重组以支持分离规则。另外，人们可以通过诱导普通知识基础的集合来提高正常规则的特征，以支持脱节规则，每个知识库具有相同的身体和一个原子。在这项工作中，我们将一组正常的知识基础称为脱节知识基础的头脑。关于是否可以使用带有头切的FixPoint构造来表征分歧混合MKNF知识库的语义是否出现问题。早些时候，我们已经证明可以将头切割与FIXPOINT运算符配对，以捕获分离的混合MKNF知识库的两值MKNF模型。三个值的语义扩展了两个值的语义，具有表达部分信息的能力。在这项工作中，我们提出了一个Fixpoint构造，该构造使用操作员迭代地捕获了三个值模型的混合MKNF知识库模型，该构造具有脱节规则。该特征还捕获了分离逻辑程序的部分稳定模型，因为程序可以表示为具有空的本体论的分离混合MKNF知识库。我们详细阐述了正常混合MKNF知识库的AFT（近似固定点理论）之间的特征和近似值之间的关系。

复杂的推理问题是使用逻辑规则最清楚，很容易指定的，但是需要具有汇总的递归规则，例如计数和总和用于实际应用。不幸的是，此类规则的含义是一个重大挑战，导致许多不同的语义分歧。本文介绍了与汇总的递归规则的统一语义，扩展了统一的基础语义和约束语义，以否定为递归规则。关键思想是支持对不同语义基础的不同假设的简单表达，并正交使用其简单的含义来解释聚合操作。我们介绍了语义的形式定义，证明了语义的重要特性，并与先前的语义相比。特别是，我们提出了对聚集的有效推断，该推论为我们从文献中研究的所有示例提供了精确的答案。我们还将语义应用于各种挑战的示例，并表明我们的语义很简单，并且在所有情况下都与所需的结果相匹配。最后，我们描述了最具挑战性的示例实验，当他们可以计算正确的答案时，表现出与知名系统相比出现的出色性能。