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

该项目的目标是开发高效的实现技术，以实现模仿人类风格常识推理的自动推理系统。自动化常识推理对于开发人工智能（AI）的高级应用非常重要，特别是在专家的思维过程需要自动化的领域，例如，医生在诊断和开药方时进行的推理。人类推理很难在计算机上模拟，因为人类通过使用默认结论（例如，如果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.