Normal Nested Answer Set Programs: Syntactics, Semantics and Logical Calculi
Gonzalo E. Imaz
TL;DR
This paper defines Normal Nested Programs (NNPs) as the Horn-headed, generally nested-body extension of normal ASP, providing a full syntactic and semantic framework that lifts NP notions to nested structures. It introduces positive-Horn nested expressions $\mathcal{H}^+_{\mathcal{L}}$ to form NNP heads, develops semantically-normal SN/NFNP correspondences, and proves that NNPs are exponentially more succinct than NP while preserving key NP properties and complexities. It also presents nested unit-resolution (NUR) and nested hyper unit-resolution (NHUR) calculi to compute answer sets directly on nested forms, showing polynomial-time computation of the least model for not-free NNPs and NP-completeness for finding answer sets. The work argues for a translator-free NASP workflow, demonstrates the potential to split disjunctive NASPs into NNPs, and outlines extensive future directions, including grounding, constraints, and broader logic extensions. Overall, the results position NNPs as a principled, efficient generalization of NP that unlocks nested expressiveness without sacrificing computational feasibility.
Abstract
Nested answer set programming (NASP; Lifschitz et al., 1999) generalizes answer set programming (ASP) by admitting nested expressions in rule bodies and heads, and thus, NASP aims at exploiting program succinctness. Yet, although NASP expressiveness is undoubtedly superior to ASP one, the former's reasoning capabilities remain unexplored. This reality seems subsequent to the next existing wide-ranging gap: normal nested programs (NNPs) are not known, or in other words, the nested normal-disjunctive boundary is unidentified thus far. Such an unfavorable situation is yet antagonistic to that of ASP as its normal programs (NPs) have been vital for propelling ASP. We will fill such a gap by defining the NNPs, their semantics and their associated nested logical calculi. Besides, while the unique known way to compute nested programs is unfold them back, we propose to do so in their original form. Firstly, we give the syntax of NNPs. For that, we initially define the positive-Horn nested-expressions and then an NNP rule as one whose head (resp. body) is a positive-Horn (resp. general) nested-expression. Secondly, we set up the semantics of NNPs by lifting to the nesting level, classical NP notions including: answer set, minimal and least model, closedness, supported-ness, immediate consequence operator and program consistency. We besides show that NNP restricted to ASP coincides with NP. Thirdly, we introduce nested logical calculi, concretely, nested unit-resolution and nested hyper unit-resolution, proving that they recover unit-resolution and hyper unit-resolution in the ASP setting. We also show how both nested logical calculi allow to process the least model of not-free NNP programs. To end, we demonstrate that computing answer sets of (resp. not-free) NNP programs is (resp. P-complete) NP-complete.