RI: Small: Answer Set Programming Modulo Theories

Arizona State University, Scottsdale AZ

Investigators

Abstract

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.