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.