论文标题
杂种ASP的聚集体和约束的均匀处理
A Uniform Treatment of Aggregates and Constraints in Hybrid ASP
论文作者
论文摘要
很难以通用方式表征混合ASP求解，因为人们需要从特定理论中抽象。受懒惰的SMT解决的启发，通常通过将理论原子视为不透明。与此不同，我们提出了一种更透明的方法，其中包括一个术语的抽象概念。我们没有通过规定某些基本属性来使它们抽象地使它们抽象，而是使它们抽象。有了这一点，我们进一步开发了一个混合ASP求解的语义框架，并为遵守不同语义原理的理论变量提供了汇总功能，表明它们将现有的汇总语义概括在ASP中，以及我们如何依靠现成的混合求解器来实现。
Characterizing hybrid ASP solving in a generic way is difficult since one needs to abstract from specific theories. Inspired by lazy SMT solving, this is usually addressed by treating theory atoms as opaque. Unlike this, we propose a slightly more transparent approach that includes an abstract notion of a term. Rather than imposing a syntax on terms, we keep them abstract by stipulating only some basic properties. With this, we further develop a semantic framework for hybrid ASP solving and provide aggregate functions for theory variables that adhere to different semantic principles, show that they generalize existing aggregate semantics in ASP and how we can rely on off-the-shelf hybrid solvers for implementation.
