RI: Small: Design and Implementation of Goal-directed Solvers for Answer Set Programming

该项目的重点是开发一个高效的答案集编程（ASP）求解器，推进基于逻辑的知识表示，逻辑编程和人工智能的最新技术。ASP是表示知识和执行高级推理（常识推理、非单调推理、计划、约束满足等）的一种优雅方式。ASP基于Gelfond和Lifschitz提出的稳定模型语义。在过去的15年里，它在知识表示（KR）和人工智能（AI）研究界获得了广泛的认可，因为它结合了否定，表达能力强，语法简单直观。过去在ASP范式的开发、实现和应用方面已经做了大量的研究。实现答案集求解器的实现技术包括从简单的基于猜测和检查的方法到基于SAT求解器和复杂启发式的方法。当前ASP系统的适用性有限由于(i)当前的实现方法不被有目的的(即不是查询驱动),(2)需要接地回答集程序如果谓词,(3)被迫找到整个程序的模型(即使回答一个给定的查询只需要计算模型的一个子集),和(iv)产生没有答案即使轻微不一致(与查询无关的)存在于知识库。该项目通过开发包含谓词的答案集程序的查询驱动实现来解决这些问题。当前的系统必须处理整个知识库（表示为答案集程序）来计算答案。与此相反，本项目中开发的查询驱动方法仅访问和处理与回答查询相关的部分知识库。查询驱动的执行允许谓词直接包含在答案集程序中。它还能提高执行效率。查询驱动的方法是基于PI小组最近发现的共归纳逻辑编程。协归纳逻辑规划赋予最大不动点计算操作语义。给定一个查询和一个答案集程序，这种基于协同归纳的操作语义用于计算包含查询目标的（部分）答案集。使用查询驱动的执行，可以直接支持谓词，也就是说，包含谓词的答案集程序不再需要首先接地。本项目的主要任务如下：(i)为命题答案集程序开发一种高效的查询驱动、自上而下的执行策略；（ii）扩展这个查询驱动的执行策略来处理Datalog ASP（不首先使程序基础）；（iii）进一步扩展这个查询驱动的执行策略来处理谓词ASP（不首先使程序搁浅）；（iv）开发ASP的共归纳扩展及其实施；(v)开发基于ASP的查询驱动的溯因推理引擎；并且，（vi）进一步扩展引擎以纳入实数约束。该研究的关键智力贡献是对答案集程序和采用否定的高级推理系统的查询驱动执行技术的调查。该研究验证了这样一种说法，即查询驱动的实现可以更优雅（更有效）地支持ASP中的约束和溯因。这项工作的更广泛影响包括知识表示的更强大应用的可用性；常识推理机制；将先进的ASP系统整合到教育和研究场所；以及研究生和本科生的研究事业发展，包括那些来自代表性不足群体的学生。

This project is focused on the development of an efficient Answer Set Programming (ASP) solver, advancing the state-of-the-art in logic based knowledge representation, logic programming and artificial intelligence. ASP is an elegant way to represent knowledge and perform advanced reasoning (common sense reasoning, non-monotonic reasoning, planning, constraint satisfaction, etc.). ASP is based on the stable model semantics proposed by Gelfond and Lifschitz. It has gained wide acceptance in the last fifteen years in the knowledge representation (KR) and artificial intelligence (AI) research communities due to its incorporation of negation, its expressiveness and simple, intuitive syntax. Considerable past research has been done in developing the ASP paradigm as well as its implementations and applications. Implementation techniques for realizing answer set solvers range from simple guess-and-check based methods to those based on SAT solvers and complex heuristics. Applicability of current ASP systems is limited due to (i) the current implementation methods not being goal-directed (i.e., not being query-driven), (ii) need for grounding the answer set program if predicates are present, (iii) being forced to find the model of the entire program (even though to answer a given query only a small subset of the model needs to be computed), and (iv) no answer being produced even if a minor inconsistency (unrelated to the query) is present in the knowledge base. This project addresses these problems by developing a query-driven implementation of answer set programs containing predicates. Current systems have to process the entire knowledge base (expressed as an answer set program) to compute an answer. In contrast, the query-driven method developed in this project only accesses and processes parts of the knowledge base that are involved in answering the query. Query-driven execution allows predicates to be directly included in answer set programs. It also leads to efficiency in execution. The query-driven method is based on PI's group's recent discovery of coinductive logic programming. Coinductive logic programming imparts operational semantics to greatest fixed point-based computations. Given a query and an answer set program, this coinduction-based operational semantics is used to compute (partial) answer sets that contain the query goal(s). With query-driven execution, predicates can be supported directly, i.e., answer set programs containing predicates no longer have to be grounded first. The main tasks of this project are the following: (i) develop an efficient query-driven, top-down execution strategy for propositional answer set programs; (ii) extend this query-driven execution strategy to handle Datalog ASP (without grounding the program first); (iii) further extend this query-driven execution strategy to handle Predicate ASP (without grounding the program first); (iv) develop coinductive extension of ASP and its implementation; (v) develop a query-driven abductive reasoning engine based on ASP; and, (vi) further extend the engine to incorporate constraints over reals. The key intellectual contributions of the research is the investigation of techniques for query-driven execution of answer set programs and advanced reasoning systems that employ negation. The research tests the claim that a query-driven implementation can more elegantly (and efficiently) support constraints and abduction in ASP. The broader impacts of this work include the availability of more powerful applications of knowledge representation; mechanisms for common sense reasoning; integration of advanced ASP systems into education and research venues; and the development of the research careers of graduate and undergraduate students, including those from under-represented groups.