RI: SMALL: Efficient Implementations of Goal-Directed Solvers for Answer Set Programming

该项目的目标是开发有效的实现技术，以实现模仿人类风格的常识推理的自动推理系统。自动化常识推理对于开发人工智能的高级应用非常重要，特别是在需要自动化专家思维过程的领域，例如，医生在诊断和开出治疗处方期间进行的推理。人类的推理很难在计算机上模拟，因为人类通过使用默认结论（例如，如果Tweety是一只鸟，它一定会飞）以及提出异常（如果Tweety后来被证明是一只企鹅，收回关于Tweety飞行能力的结论）来简化推理。由于人类推理的这种特殊性质，基于标准逻辑的方法并不能很好地发挥作用：人们不得不求助于非单调逻辑，也就是说，在这种逻辑中，现在得出的结论可能会在以后获得新信息时被撤回。在这个项目中进行的研究将导致这些非单调逻辑的高效、查询驱动的实现。该项目的成功完成将带来先进的应用，例如可以向医生建议如何治疗特定疾病的自动化系统，或者可以模仿人类驾驶专业知识的自动驾驶汽车决策系统。该项目将依靠答案集编程（ASP）的范式来表示常识性知识。答案集程序由包含（可能是否定的）谓词的规则组成。目前的ASP系统依赖于首先建立答案集程序来获得等价的命题程序，然后使用布尔可满足性（SAT）求解器来找到包含用户所寻求的答案的命题程序的模型。接地要求限制了可以执行的程序的范围。该项目建立在早期对直接执行谓词回答集程序的研究之上，即不首先将它们接地。它的目的是通过设计一个虚拟机来实现这些系统的更快的实现，答案集程序将被编译并执行。

The goal of this project is to develop efficient implementation techniques for realizing automated reasoning systems that emulate human-style common sense reasoning. Automating common sense reasoning is important for developing advanced applications of artificial intelligence (AI), particularly, in areas where the thought process of an expert needs to be automated, e.g., reasoning performed by a medical doctor during diagnosis and prescribing a treatment. Human reasoning is difficult to emulate on a computer, as humans simplify reasoning by using default conclusions (e.g., if Tweety is a bird, it must fly) coupled with raising exceptions (if Tweety turns out to be a penguin later, retract the conclusion about Tweety's flying abilities). Because of this peculiar nature of human reasoning, approaches based on standard logic do not work very well: one has to resort to a non-monotonic logic, i.e., a logic in which conclusions reached now may be withdrawn later as new information becomes available. Research conducted in this project will result in efficient, query-driven implementations of these non-monotonic logics. Successful completion of this project will result in advanced applications such as an automated system that can advise a physician on how to treat a particular disease, or a self-driving car's decision-making system that can emulate a human's driving expertise.The project will rely on the paradigm of answer set programming (ASP) to represent common sense knowledge. An answer set program consists of rules containing (possibly negated) predicates. Current ASP systems rely on first grounding the answer set program to obtain an equivalent propositional program, and then using a Boolean satisfiability (SAT) solver to find models of this propositional program that contain the answer that is sought by the user. The grounding requirement restricts the range of programs that can be executed. This project builds upon earlier research on directly executing predicate answer set programs, i.e., without grounding them first. It aims to realize faster implementations of such systems by designing a virtual machine to which an answer set programs will be compiled to and executed.