关于递归程序
On finitely recursive programs
摘要：
析取有限程序是一类逻辑程序，它允许函数符号，因此允许无限域。它们具有非常好的计算特性，例如，地面查询是可判定的，而在一般情况下，稳定模型语义是高度不可判定的。本文证明了一类更大的程序，称为递归程序，在稳定模型语义下，它保持了有限程序的大部分优良性质，即：（i）递归程序具有紧致性;（ii）不一致性检查和怀疑推理是半判定的;（iii）正常递归程序的怀疑归结是完全的.此外，我们展示了如何检查不一致性，并回答怀疑查询使用有限子集的地面程序实例。我们通过推广Lifschitz和Turner的分裂序列定理来实现这一点：我们证明了如果输入程序P是递归的，则由任何光滑分裂ω序列确定的部分稳定模型收敛到P的稳定模型。
英文摘要：
Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable model semantics is highly undecidable. In this paper we prove that a larger class of programs, called finitely recursive programs, preserves most of the good properties of finitary programs under the stable model semantics, namely: (i) finitely recursive programs enjoy a compactness property; (ii) inconsistency checking and skeptical reasoning are semidecidable; (iii) skeptical resolution is complete for normal finitely recursive programs. Moreover, we show how to check inconsistency and answer skeptical queries using finite subsets of the ground program instantiation. We achieve this by extending the splitting sequence theorem by Lifschitz and Turner: We prove that if the input program P is finitely recursive, then the partial stable models determined by any smooth splitting omega-sequence converge to a stable model of P.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
