Safe Formulas in the General Theory of Stable Models

TL;DR

This paper explores safe formulas in the general theory of stable models, showing their equivalence to grounded, variable-free sentences and characterizing their stable models through simple syntactic formulas.

Contribution

It demonstrates that safe first-order formulas are equivalent to their groundings and provides a syntactic characterization of their stable models.

Findings

Safe formulas are equivalent to their groundings.

Stable models of safe formulas can be characterized syntactically.

Grounding preserves stable models for safe formulas.

Abstract

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.