Functional Stable Model Semantics and Answer Set Programming Modulo Theories
Provides a theoretical foundation for integrating intensional functions into answer set programming, benefiting researchers in knowledge representation and reasoning.
The paper shows that functional stable model semantics is key to integrating answer set programming with satisfiability modulo theories (ASPMT), and that tight ASPMT programs can be translated into SMT instances, analogous to the ASP-to-SAT relationship.
Recently there has been an increasing interest in incorporating ``intensional'' functions in answer set programming. Intensional functions are those whose values can be described by other functions and predicates, rather than being pre-defined as in the standard answer set programming. We demonstrate that the functional stable model semantics plays an important role in the framework of ``Answer Set Programming Modulo Theories (ASPMT)'' -- a tight integration of answer set programming and satisfiability modulo theories, under which existing integration approaches can be viewed as special cases where the role of functions is limited. We show that ``tight'' ASPMT programs can be translated into SMT instances, which is similar to the known relationship between ASP and SAT.