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 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.

翻译：在经典逻辑中，非布尔流值（如物体的位置）可通过函数自然描述。然而，在回答集程序中并非如此——其中函数的值是预定义的，且语义的非单调性与谓词外延的最小化相关，而与函数无关。我们将Ferraris、Lee和Lifschitz提出的一阶稳定模型语义扩展至允许内涵函数——即像谓词那样通过逻辑程序规范的函数。我们证明，稳定模型语义的许多已知性质可自然扩展至该形式体系，并将其与其它引入内涵函数的相关方法进行比较。此外，我们以此扩展为基础定义模理论回答集编程（ASPMT），其方式类似于可满足性模理论（SMT）的定义，从而允许在ASP框架中实现类似SMT的高效一阶推理。通过利用涉及函数的SMT求解技术，ASPMT可应用于包含实数的领域，并缓解基础问题。我们证明，将ASP与CSP/SMT集成的其它方法可归结为ASPMT中函数限于非内涵情形的特例。