SGER: Grounding-Independent Reasoning in Answer Set Programming

答案集编程是一种重要的、实用的声明式编程范式，广泛应用于知识密集型应用。然而，通过接地消除变量的要求限制了建模和推理能力，并可能产生大型的、难以理解的命题逻辑程序。本课题通过将传统的稳定模型语义与经典逻辑相结合，突破了答案集规划的局限。该项目包括，例如，(i)安全条件的研究，在这种条件下，一阶推理可以简化为命题推理，这证明了使用答案集求解器进行独立推理；（ii）带变量的循环公式的研究，这将允许稳定模型的计算由一阶定理证明。该项目的成功将对需要独立推理的广泛领域产生重大影响，例如使用背景知识的问答系统，以及规划和描述逻辑。

Answer set programming is an important, practical declarative programming paradigm widely applied to knowledge-intensive applications. However, the requirement that variables be eliminated through grounding limits modeling and reasoning capabilities, and can yield large, incomprehensible propositional logic programs. This project aims beyond the limitations of answer set programming by merging the traditional stable model semantics with classical logic. The project includes, for example, (i) the study of safety conditions, under which first-order reasoning can be reduced to propositional reasoning, which justifies the use of answer set solvers for grounding-independent reasoning; (ii) the study of loop formulas with variables, which will allow stable models to be computed by first-order theorem provers. The success of this project will have a significant impact on a wide range of domains that requires grounding-independent reasoning, such as Question & Answer systems that use background knowledge, as well as planning and description logics.