用SMT求解器实现带理论的答案集编程，支持连续变量推理。
System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
- 将ASPMT程序转化为SMT实例，借助Z3求解
- 可处理实数计算，支持连续变化的推理
- 适合需精确数值逻辑推理的研究者
答案集编程模理论（ASPMT）是一种结合答案集编程与满足模理论的方法，基于函数稳定模型语义。研究表明，ASPMT程序的紧致片段可转换为SMT实例，从而利用SMT求解器计算其稳定模型。本文提出名为{ t aspsmt2smt}的编译器，实现了该转换过程。系统使用ASP接地工具{ t gringo}对输入程序部分接地，并将剩余变量交由{ t z3}处理。实验表明，该系统能有效处理实数计算，适用于连续变化的推理任务。
原文摘要 · Abstract (English)
Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable models of ASPMT programs. In this paper we present a compiler called {\sc aspsmt2smt}, which implements this translation. The system uses ASP grounder {\sc gringo} and SMT solver {\sc z3}. {\sc gringo} partially grounds input programs while leaving some variables to be processed by {\sc z3}. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。