Safe Formulas in the General Theory of Stable Models
This work provides a theoretical foundation for improving answer set solvers, though it is incremental as it extends existing concepts of safe rules.
The paper tackles the problem of grounding safe first-order formulas in answer set programming by proving that any safe sentence is equivalent to its grounded form, ensuring they share the same stable models and enabling characterization by simpler syntactic forms.
Safe first-order formulas generalize the concept of a safe rule, which plays an important role in the design of answer set solvers. We show that any safe sentence is equivalent, in a certain sense, to the result of its grounding -- to the variable-free sentence obtained from it by replacing all quantifiers with multiple conjunctions and disjunctions. It follows that a safe sentence and the result of its grounding have the same stable models, and that the stable models of a safe sentence can be characterized by a formula of a simple syntactic form.