Knowledge Representation and Reasoning: Pushing the 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.