Knowledge Representation and Reasoning: Pushing the Frontier

知识表示和推理：推动前沿

• 批准号: RGPIN-2020-05211
• 负责人: You, JiaHuai
• 金额: $ 2.11万
• 依托单位: University of Alberta
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=717054
• 关键词: Knowledge; Representation; Reasoning; Pushing; Frontier

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.

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