使用声音应答包容功能制表
Tabling with Sound Answer Subsumption
摘要：
Tabling是逻辑程序的一种强大的解析机制，它比普通的Prolog更忠实地捕捉它们的最小不动点语义。在许多制表应用程序中，我们对一个目标的所有答案的集合不感兴趣，而只需要这些答案的聚合。一些作品已经研究了有效的技术，如基于格的答案包容和模式导向制表，这样做的各种形式的聚合。虽然对不同方法的表现力和有效实施给予了很大的关注，但没有考虑到合理性。本文表明，不同的实现确实无法产生最小不动点的一些程序。作为一种补救措施，我们提供了一个正式的框架，概括现有的方法，我们建立了一个健全的标准，解释了程序的方法是健全的。本条款正在考虑在TPLP中接受。
英文摘要：
Tabling is a powerful resolution mechanism for logic programs that captures their least fixed point semantics more faithfully than plain Prolog. In many tabling applications, we are not interested in the set of all answers to a goal, but only require an aggregation of those answers. Several works have studied efficient techniques, such as lattice-based answer subsumption and mode-directed tabling, to do so for various forms of aggregation. While much attention has been paid to expressivity and efficient implementation of the different approaches, soundness has not been considered. This paper shows that the different implementations indeed fail to produce least fixed points for some programs. As a remedy, we provide a formal framework that generalises the existing approaches and we establish a soundness criterion that explains for which programs the approach is sound. This article is under consideration for acceptance in TPLP.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
