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

该项目的目标是开发高效的实现技术，以实现模仿人类风格的常识推理的自动推理系统。自动化常识推理对于开发人工智能(AI)的高级应用非常重要，特别是在需要自动化专家的思维过程的领域，例如由医生在诊断和开出治疗期间执行的推理。人类的推理很难在计算机上模仿，因为人类通过使用默认结论(例如，如果Twety是一只鸟，它必须飞)和提出例外(如果Twety后来被证明是一只企鹅，收回关于Twety飞行能力的结论)来简化推理。由于人类推理的这种特殊性质，基于标准逻辑的方法不能很好地工作：人们必须求助于非单调逻辑，即，随着新信息的获得，现在得出的结论可能会在以后被撤回。本项目中进行的研究将导致这些非单调逻辑的高效、查询驱动的实现。该项目的成功完成将带来先进的应用，如可以建议医生如何治疗特定疾病的自动化系统，或者可以模仿人类驾驶专业知识的自动驾驶汽车决策系统。该项目将依赖于答案集编程(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.