RI: Small: Answer Set Programming Modulo Theories

Project: Research project

Project Details


Answer set programming (ASP) is one of the most successful declarative programming methods, which has been used in many areas of science and technology. Effective computation of answer sets is largely due to intelligent grounding methods and efficient search methods originated from the design of SAT solvers. However, the widespread use of ASP inspired several extensions to the ASP languages and computational tools which require going beyond this setting. Examples include interface with external information source that do not rely on grounding (e.g., ontology knowledge bases), and integration with tools of other computing paradigms (e.g., constraint solvers and SMT solvers). While the research community is beginning to understand the importance of integrating ASP with other computing paradigms, due to the nonmonotonic nature of the stable model semantics, it is non-trivial to define reasonable semantics for such extensions. We claim that the main obstacle is due to the fact that the traditional ASP was centered around propositional semantics, and does not treat functions in a proper way. The aim of this proposal is to correct this deficiency in ASP and use it as a basis of the framework for ASP modulo theories, in analogous with the work on Satisfiability Modulo Theories. Intellectual Merit. The success of the project will provide a uniform framework that opens the door to the creation of a powerful declarative programming paradigm, leveraging the ability to represent and reason about qualitative, commonsensical and numerical knowledge in an efficient way. The proposed research will relate ASP to other related computing paradigms. Integrating ASP with SMT will overcome the computational limitations of ASP. It will allow SMT solvers to be used for expressive nonmonotonic reasoning involving quantitative information. The high level language that we design for describing hybrid systems will facilitate automated reasoning about hybrid systems, and the new generation of ASP solvers that employ SMT technologies will be applied to computing hybrid systems. Broader Impacts The use of solving techniques from other research communities is likely to promote cross-fertilization among the involved communities. The system prototypes will be freely available as open source software. The results of our research, including a system demonstration, will be disseminated via a tutorial collocated with a major conference in AI, and presented at other conferences and in journal papers. Many students and researchers will be involved in our work through participation in Texas Action Group. The research will also involve both graduate and undergraduate students, contributing to a strengthened relationship between education and research. By getting involved in different aspects of the project, students will be trained in a critical area of information and knowledge management, thereby enhancing their careers and contributing to their professional growth. The project, which actively involves under-represented minorities, will impact several existing university courses. Keywords: answer set programming; satisfiability modulo theories 1
Effective start/end date8/15/137/31/17


  • National Science Foundation (NSF): $315,000.00

Fingerprint Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.