用ASPMT统一处理连续与离散变化，让逻辑编程更懂动态系统。
Answer Set Programming Modulo Theories and Reasoning about Continuous Changes
- 将ASP与SMT融合，通过功能稳定模型语义统一处理复杂变化。
- 成功将行动语言C+升级为支持连续资源累积效应的推理框架。
- 适合做动态系统建模、智能规划与自动化推理的研究者使用。
答案集编程模理论（ASPMT）是答案集编程（ASP）与可满足性模理论（SMT）紧密集成的新框架。它基于对背景理论解释的固定，借鉴函数稳定模型语义的最新提案，类似一阶逻辑与SMT的关系。如同ASP与SAT之间的关系，'紧致'的ASPMT程序可被转化为SMT实例。我们通过增强行动语言C+以处理连续变化和离散变化来展示ASPMT的实用性。我们将C+的语义重新表述为ASPMT形式，并证明可使用SMT求解器进行计算。此外，该语言还能表示连续资源上的累积效应。
原文摘要 · Abstract (English)
Answer Set Programming Modulo Theories (ASPMT) is a new framework of tight integration of answer set programming (ASP) and satisfiability modulo theories (SMT). Similar to the relationship between first-order logic and SMT, it is based on a recent proposal of the functional stable model semantics by fixing interpretations of background theories. Analogously to a known relationship between ASP and SAT, ``tight'' ASPMT programs can be translated into SMT instances. We demonstrate the usefulness of ASPMT by enhancing action language C+ to handle continuous changes as well as discrete changes. We reformulate the semantics of C+ in terms ofASPMT, and show that SMT solvers can be used to compute the language. We also show how the language can represent cumulative effects on continuous resources.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。