TY - JOUR
T1 - First-order stable model semantics with intensional functions
AU - Bartholomew, Michael
AU - Lee, Joohyung
N1 - Funding Information:
We are grateful to Yi Wang and Nikhil Loney for many useful discussions and to the anonymous referees for their constructive comments. This work was partially supported by the National Science Foundation under Grants IIS-1526301 , and IIS-1815337 . Appendix A
Publisher Copyright:
© 2019 Elsevier B.V.
PY - 2019/8
Y1 - 2019/8
N2 - In classical logic, nonBoolean fluents, such as the location of an object, can be naturally described by functions. However, this is not the case in answer set programs, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions—functions that are specified by a logic program just like predicates are specified. We show that many known properties of the stable model semantics are naturally extended to this formalism and compare it with other related approaches to incorporating intensional functions. Furthermore, we use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT), analogous to the way that Satisfiability Modulo Theories (SMT) is defined, allowing for SMT-like effective first-order reasoning in the context of Answer Set Programming (ASP). Using SMT solving techniques involving functions, ASPMT can be applied to domains containing real numbers and alleviates the grounding problem. We show that other approaches to integrating ASP and CSP/SMT can be related to special cases of ASPMT in which functions are limited to non-intensional ones.
AB - In classical logic, nonBoolean fluents, such as the location of an object, can be naturally described by functions. However, this is not the case in answer set programs, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions—functions that are specified by a logic program just like predicates are specified. We show that many known properties of the stable model semantics are naturally extended to this formalism and compare it with other related approaches to incorporating intensional functions. Furthermore, we use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT), analogous to the way that Satisfiability Modulo Theories (SMT) is defined, allowing for SMT-like effective first-order reasoning in the context of Answer Set Programming (ASP). Using SMT solving techniques involving functions, ASPMT can be applied to domains containing real numbers and alleviates the grounding problem. We show that other approaches to integrating ASP and CSP/SMT can be related to special cases of ASPMT in which functions are limited to non-intensional ones.
KW - Answer set programming
KW - Intensional functions
KW - Satisfiability modulo theories
UR - http://www.scopus.com/inward/record.url?scp=85062148233&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85062148233&partnerID=8YFLogxK
U2 - 10.1016/j.artint.2019.01.001
DO - 10.1016/j.artint.2019.01.001
M3 - Article
AN - SCOPUS:85062148233
SN - 0004-3702
VL - 273
SP - 56
EP - 93
JO - Artificial Intelligence
JF - Artificial Intelligence
ER -