Normal Nested Answer Set Programs: Syntactics, Semantics and Logical Calculi

TL;DR

This paper introduces normal nested answer set programs (NNPs), defining their syntax, semantics, and logical calculi, and demonstrates their computational complexity and relation to existing answer set programming frameworks.

Contribution

It fills the gap by formally defining NNPs, their semantics, and logical calculi, extending answer set programming to nested normal-disjunctive programs.

Findings

NNPs generalize ASP with nested expressions.

Answer set computation for NNPs is P-complete.

Nested logical calculi recover classical resolution methods.

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.