将可描述函数引入答案集编程，提升理论集成能力
Functional Stable Model Semantics and Answer Set Programming Modulo Theories
- 用可定义函数扩展答案集编程框架
- 证明紧致ASPMT程序可转为SMT实例
- 适合逻辑编程与形式化验证研究者
近年来，答案集编程中对“内涵函数”的关注日益增加。这类函数的值可通过其他函数和谓词描述，而非预先定义。我们证明，功能性稳定模型语义在“答案集编程模理论（ASPMT）”框架中起关键作用——该框架是答案集编程与满足性模理论的紧密整合，现有整合方法均可视为函数作用受限的特例。我们进一步证明，‘紧致’ASPMT程序可转化为SMT实例，类似于经典答案集编程与SAT之间的对应关系。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。