Knowledge Representation and Reasoning: Pushing the Frontier

知识表示和推理（KRR）是人工智能的一个领域，致力于通过用建模语言表示计算问题来解决问题，并配备计算机软件来处理用该语言编写的代码。这些语言在解决重要的实际问题上有很大的潜力，例如，用网络推理的问题。为了实现这些潜力，在本研究中，我们建议从三个方向研究一系列问题。在第一个方向，我们将采取最基本的推理任务，命题可满足性（SAT）。问题是确定命题逻辑中的公式是否可满足。SAT在计算科学中具有核心重要性，其应用范围从电路验证到软件诊断和人工智能规划。SAT求解技术在其他KRR语言的推理方法方面取得了重大进展。因此，几十年来，构建高效的SAT求解器一直是许多研究人员的圣杯。我们的研究目标是推进最先进的SAT解决方案。我们工作的初步成功已经在最近的SAT竞赛中得到了证明，即2019年SAT竞赛，我们的一份参赛作品已经进入了顶级行列。接下来，我们提出研究答案集规划（ASP）中的成本最优规划。ASP是一种面向解决计算困难问题的问题解决范式，被认为是KRR领域的一个有前途的发展方向。目前，最先进的ASP计划是基于makespan -一个限制计划中允许的步骤数量的数字。理想情况下，我们想要一种方法来规划，保证一个全局最优的解决方案，而不提及最大完工时间。基于SAT/ asp的规划的文献几乎是空白的这种方法的可能性。在本研究中，我们将从理论和实践两个方面着手，基于ASP构建高效的成本最优规划器。在第三个方向上，我们建议将我们当前的研究推向新的领域，其中包括对存在规则的分布式推理的研究。存在规则语言为许多应用程序提供了建模工具，而分布式推理是释放语义web应用程序强大功能的关键。我们的目标是扩展分布式推理在现实世界本体中的适用性，并演示其实际有效性。总之，在本研究中，我们将解决一些在一些重要的KRR语言中出现的表示和推理问题，从SAT到ASP中的成本最优规划，再到存在规则推理。预计我们的SAT求解技术将成为最先进的技术的一部分，我们在成本最优规划方面的努力将扩大ASP的适用性，我们现有研究的推动将为该领域带来新的知识。

Knowledge representation and reasoning (KRR) is a field of Artificial Intelligence dedicated to problem solving by representing computational problems in a modelling language equipped with computer software for processing code written in the language. There are great potentials for these languages for solving significant practical problems, e.g., the problem of reasoning with the web. To realize some of these potentials, in this research we propose to investigate a range of issues in three directions. In the first direction, we will take up the most fundamental reasoning task, Propositional Satisfiability (SAT). The problem is to determine whether a formula in propositional logic is satisfiable. SAT is of central importance in Computing Science with applications ranging from circuit verification to software diagnosis and AI planning. SAT solving techniques have made a significant inroad into reasoning methods for other KRR languages. Hence, building efficient SAT solvers has been a holy grail of many researchers for decades. The goal of our research is to advance the state-of-the-art in SAT solving. The initial success of our work has been demonstrated in the latest SAT Competition, SAT Race 2019, where one of our submissions has made to the top tier. Next, we propose to investigate cost-optimal planning in Answer Set Programming (ASP). ASP is a paradigm of problem solving oriented towards solving computationally hard problem and has been considered a promising development in KRR. Currently, the state-of-the-art ASP planners are based on makespan - a number limiting the allowed number of steps in a plan. Ideally, we want an approach to planning that guarantees a globally optimal solution without mention of makespan. The literature of SAT/ASP-based planning is almost blank on the possibility of such an approach. In this research, we will tackle both theoretical and practical fronts and build efficient cost-optimal planners based on ASP. In the third direction, we propose to push our current research to new frontiers, which includes a study of distributed reasoning with existential rules. Existential rule languages provide a modeling tool for many applications, yet distributed reasoning is a key to unleashing the power of semantic web applications. Our goal here is to extend the applicability and demonstrate the practical effectiveness of distributed reasoning with real-world ontologies. In summary, in this research we will address a number of representation and reasoning issues that arise in some important KRR languages, from SAT to cost-optimal planning in ASP to reasoning with existential rules. It is expected that our SAT solving techniques will become part of the state-of-the-art, our effort on cost-optimal planning will expand the applicability of ASP, and the push of our existing research to new frontiers will bring new knowledge to the field.