First-order stable model semantics with intensional functions
First-order stable model semantics with intensional functions
复制标题
DOI：
10.1016/j.artint.2019.01.001
复制
发表时间：
2019-08
期刊：
影响因子：
--
通讯作者：
M. Bartholomew;Joohyung Lee
中科院分区：
文献类型：
--
作者：
M. Bartholomew;Joohyung Lee
在经典逻辑中，非布尔流语（例如对象的位置）可以自然地用函数来描述。然而，在答案集程序中情况并非如此，其中函数的值是预先定义的，并且语义的非单调性与最小化谓词的范围有关，但与函数无关。我们扩展了 Ferraris、Lee 和 Lifschitz 的一阶稳定模型语义，以允许内涵函数——由逻辑程序指定的函数，就像指定谓词一样。我们表明，稳定模型语义的许多已知属性可以自然地扩展到这种形式主义，并将其与其他合并内涵函数的相关方法进行比较。此外，我们使用此扩展作为定义答案集编程模理论 (ASPMT) 的基础，类似于定义可满足性模理论 (SMT) 的方式，允许在答案集编程 (ASP) 的上下文中进行类似 SMT 的有效一阶推理。使用涉及函数的 SMT 求解技术，ASPMT 可以应用于包含实数的域并缓解接地问题。我们表明，集成 ASP 和 CSP/SMT 的其他方法可能与 ASPMT 的特殊情况相关，其中功能仅限于非内涵功能。
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 definingAnswer Set ProgrammingModulo 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.