Splitting Answer Set Programs with respect to Intensionality Statements (Extended Version)

TL;DR

Addresses splitting of first-order ASP-like theories with respect to intensionality statements $\lambda$ by introducing $EM(\lambda)$ and a context-aware splitting framework. Proposes dependency graphs $\mathfrak{G}_{\Lambda}$ and $\mathfrak{G}_{\Lambda,\Psi}$ and semantic approximators $\Psi$ to prove a generalized Splitting Theorem for both disjunctive programs and arbitrary theories, with precise tools $Sp_{\Psi}$, $Pnn_{\Psi}$, and $Nnn_{\Psi}$. Provides a formal theory of splitting that covers modular encodings and meta-encodings, including a local-to-global Splitting Lemma and a general Splitting Theorem, and demonstrates how to recover classic results in the propositional/disjunctive case. The work enables modular solving and correctness proofs for ASP encodings that depend on time, initial-state conditions, or context, while acknowledging undecidability barriers in general semantic checks and pointing toward automated theorem proving for verification.

Abstract

Splitting a logic program allows us to reduce the task of computing its stable models to similar tasks for its subprograms. This can be used to increase solving performance and prove program correctness. We generalize the conditions under which this technique is applicable, by considering not only dependencies between predicates but also their arguments and context. This allows splitting programs commonly used in practice to which previous results were not applicable.

Theorems & Definitions (30)

• Proposition 1
• Theorem 1: Splitting disjunctive programs
• Proposition 2
• Theorem 2: Splitting Theorem
• Proposition 3
• Lemma 1
• Proposition 4
• Lemma 2
• Lemma 3
• Lemma 4