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.
