带函数的选言ASP:可判定性和有效计算
Disjunctive ASP with Functions: Decidable Queries and Effective Computation
摘要:
一般来说,查询具有函数的分离式ASP是一项高度不可判定的任务。在本文中,我们专注于分层否定和功能的析取逻辑程序下的稳定模型语义(ASP^{fs})。我们表明,在这种设置下的查询回答是可判定的,如果查询是递归的(ASP^{fs}_{fr})。我们的证明收益率也是一个有效的查询评估方法。这是通过将魔术集技术扩展到ASP^{fs}_{fr}来实现的。我们表明,魔术集重写程序查询相当于原来的(勇敢和谨慎的推理下)。此外,我们证明了重写程序也是可判定的,这意味着它是可判定的。重要的是,可使用现有的ASP求解器来评估基础程序,从而使ASP^{fs}_{fr}查询类在实践中可用。
英文摘要:
Querying over disjunctive ASP with functions is a highly undecidable task in general. In this paper we focus on disjunctive logic programs with stratified negation and functions under the stable model semantics (ASP^{fs}). We show that query answering in this setting is decidable, if the query is finitely recursive (ASP^{fs}_{fr}). Our proof yields also an effective method for query evaluation. It is done by extending the magic set technique to ASP^{fs}_{fr}. We show that the magic-set rewritten program is query equivalent to the original one (under both brave and cautious reasoning). Moreover, we prove that the rewritten program is also finitely ground, implying that it is decidable. Importantly, finitely ground programs are evaluable using existing ASP solvers, making the class of ASP^{fs}_{fr} queries usable in practice.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。