Stable Models for Infinitary Formulas with Extensional Atoms

TL;DR

This paper extends the concept of stable models for infinitary propositional formulas by distinguishing between intensional and extensional atoms, and generalizes the symmetric splitting theorem to infinitary formulas.

Contribution

It introduces a new distinction between intensional and extensional atoms in stable models for infinitary formulas and extends the symmetric splitting theorem to this setting.

Findings

Enhanced stable model definition with atom distinction

Extended symmetric splitting theorem to infinitary formulas

Facilitates reasoning about infinitary definitions

Abstract

The definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition by introducing a distinction between intensional and extensional atoms. The symmetric splitting theorem for first-order formulas is then extended to infinitary formulas and used to reason about infinitary definitions. This note is under consideration for publication in Theory and Practice of Logic Programming.