RI: Small: Answer Set Programming Modulo Theories

表达型非单调一阶推理的有效计算对于实现鲁棒智能具有重要意义。回答集编程（ASP）是一种成功的非单调声明式编程范式，但由于其命题设置，在处理涉及函数的一阶推理方面受到限制。可满足性模理论（SMT）是一种成功的解决一阶推理问题的方法，但在处理非单调推理问题上存在局限性，本课题旨在通过将ASP和SMT紧密结合在“答案集编程模理论”（ASPMT）框架中来弥补这些不足。ASPMT将享受ASP建模语言的表现力，同时利用SMT和其他相关计算范例中可用的有效约束/理论求解方法。它将提供一个可行的方法来解决问题，需要离散的高级推理和连续的低级推理，并将提供一个有效的方式来处理异构的知识和/或计算源在一个统一的框架。该项目还将提供该框架的在线计算模型及其实现。该项目的成功将通过智能地组合不同的形式主义及其实现来产生一种有效计算表达性推理的通用方法，并将促进相关社区之间的相互促进。这个项目的成功将对广泛的领域产生重大影响，这些领域可以从强大的声明式编程范式中受益。它将提供一个实际可用的知识表示编程语言和工具，可以很容易地被非KR专家使用，同时隐藏各种计算方法的细节。

Efficient computation of expressive nonmonotonic first-order reasoning is important for realizing robust intelligence. Answer Set Programming (ASP) is a successful nonmonotonic declarative programming paradigm, but is limited in handling first-order reasoning involving functions due to its propositional setting. Satisfiability Modulo Theories (SMT) is a successful approach to solving some specialized first-order reasoning, but is limited in handling nonmonotonic reasoning.This project aims at correcting these deficiencies by tightly integrating ASP and SMT in the framework of "Answer Set Programming Modulo Theories" (ASPMT). ASPMT will enjoy the expressiveness of the ASP modeling language while leveraging efficient constraint / theory solving methods available in SMT and other related computing paradigms. It will provide a viable approach to solving problems that requires both discrete high level reasoning and continuous low level reasoning, and will provide an effective way to handle heterogeneous knowledge and/or computation sources in a uniform framework. The project will also deliver an online computation model of the framework and its implementation.The success of the project will produce a general method of efficient computation of expressive reasoning by intelligently combining different formalisms and their implementations, and will promote cross-fertilization among the involved communities. The success of this project will have a significant impact on a wide range of domains that can benefit from a powerful declarative programming paradigm. It will provide a practically usable knowledge representation programming language and tools, which can be easily used by non-KR experts while hiding the details of various computational methods.