Polynomial Approximation to Well-Founded Semantics for Logic Programs with Generalized Atoms: Case Studies

The well-founded semantics of normal logic programs has two main utilities, one being an efficiently computable semantics with a unique intended model, and the other serving as polynomial time constraint propagation for the computation of answer sets of the same program. When logic programs are generalized to support constraints of various kinds, the semantics is no longer tractable, which makes the second utility doubtful. This paper considers the possibility of tractable but incomplete methods, which in general may miss information in the computed result, but never generates wrong conclusions. For this goal, we first formulate a well-founded semantics for logic programs with generalized atoms, which generalizes logic programs with arbitrary aggregates/constraints/dl-atoms. As a case study, we show that the method of removing non-monotone dl-atoms for the well-founded semantics by Eiter et al. actually falls into this category. We also present a case study for logic programs with standard aggregates.

1. 1.

   This assumes that the satisfaction of a generalized atom by one interpretation can be determined in polynomial time.

2. 2.

   Generalized atoms in [2] are essentially conjunctions of generalized atoms defined here.

3. 3.

   Domain is needed primarily for complexity measures. It is also indirectly involved in the notion of satisfaction, which gives the semantics of a generalized atom.

4. 4.

   This is to be consistent with the notion of an extension of a partial interpretation introduced in [11].

5. 5.

   For simplicity, we assume that equality does not appear in rules.

6. 6.

   This example was originally provided by Yisong Wang.

7. 7.

   http://www.cs.uni-potsdam.de/clasp/.

Authors and Affiliations

1. Department of Computing Science, University of Alberta, Edmonton, Canada

   Md. Solimul Chowdhury, Arash Karimi & Jia-Huai You

2. College of Computer and Information Science, Shanghai University, Baoshan, China

   Fangfang Liu

3. College of Computer and Information Science, Southwest University, Chongqing, China

   Wu Chen

Corresponding author

Correspondence to Md. Solimul Chowdhury .

Editors and Affiliations

1. IASI-CNR, Rome, Italy

   Maurizio Proietti

2. Nagoya Institute of Technology, Nagoya, Japan

   Hirohisa Seki

A Appendix: Proof of Theorem 1

Proof

We prove the claim by induction on the construction of \(\textit{lfp}(W_{\pi (\textit{KB})})\) and \(\textit{lfp}(W_{\textit{KB}})\).

1. (a)

   Base: \(W^0_{\pi (\textit{KB})}|_\tau = W^0_\textit{KB}= \emptyset \).

2. (b)

   Step: Assume, for all \(k \ge 0\), \(W^k_{\pi (\textit{KB})}|_\tau \subseteq W^k_\textit{KB}\), and prove \(W^{k+1}_{\pi (\textit{KB})}|_\tau \subseteq W^{k+1}_\textit{KB}\). By definition, we know

To prove \(W^{k+1}_{\pi (\textit{KB})}|_\tau \subseteq W^{k+1}_\textit{KB}\), it is sufficient to prove both of

Below, let us assume that at most one dl-atom may appear in a rule. The proof can be generalized to arbitrary rules by the same argument, for the transformation of one dl-atom at a time.

1. (i)

   We first prove (5). Let \(a \in T_{\pi (\textit{KB})} (W^k_{\pi (\textit{KB})}) |_\tau \). By definition, \(\exists r' \in \pi (P)\) such that \(B(r')\) is persistently true under \(W^k_{\pi (\textit{KB})}\). WLOG, assume for some \(r \in P\), \(\pi (r) = \{r',r''\}\), as illustrated in (7) below, in which a dl-atom appears positively, which is replaced by rules in (7) of \(\pi (r)\).

   $$\begin{aligned}&r:~ a \leftarrow \ldots , DL [ \ldots , S_j {\cap \!\!\!\!-} p_j , \ldots ; Q](e), \ldots \end{aligned}$$

   (7)
   $$\begin{aligned}&r':a \leftarrow \ldots , DL [ \ldots , S_j {\cup \!\!\!\!-} \bar{p_j}, \ldots ; Q](\mathbf{e}), \ldots \nonumber \\&r'':\bar{p_j} (\mathbf{e}) \leftarrow \lnot DL [S^{\prime }_j \uplus {p_j}; S^{\prime }](\mathbf{e}) \end{aligned}$$

   (8)

   Let \(D\) denote the dl-atom in (7), and \(D'\) the corresponding dl-atom in (7). If the operator \({\cap \!\!\!\!-}\) does not occur in \(D\), then trivially \(B(r)\) is persistently true under \(W^k_\textit{KB}\), and thus \(a \in T_\textit{KB}(W^k_\textit{KB})\).

   Otherwise, since \(B(r')\) is persistently true under \(W^k_{\pi (\textit{KB})}\), we have \(D'\) is persistently true under \(W^k_{\pi (\textit{KB})}\), and by the fact that \(D'\) is monotone, we have \(W^k_{\pi (\textit{KB})} \models _L D'\). The atom \(\bar{p_j} (\mathbf{e})\) may or may not play a role in the entailment \(L\cup \bigcup _{i=1}^m D'_i \models Q(\mathbf{e})\) (cf. Definition (6)). The proof is trivial if it does not. Otherwise, \(\bar{p_j} (\mathbf{e})\) is well-founded already w.r.t. \(W^k_{\pi (\textit{KB})}\), and by the last rule in (7), \(p_j(\mathbf{e})\) is unfounded w.r.t. \(W^{k'}_{\pi (\textit{KB})}\), for some \(k' < k\). By induction hypothesis, we know \(W^{k'}_{\pi (\textit{KB})} |_\tau \subseteq W^{k'}_\textit{KB}\), thus \(p_j(\mathbf{e})\) is unfounded w.r.t. \(W^k_\textit{KB}\). It follows \(D\) is persistently true under \(W^k_\textit{KB}\), and by the assumption that \(D\) is the only dl-atom in (7) and that \(B(r')\) is persistently true under \(W^k_{\pi (\textit{KB})}\), we have \(B(r)\) is persistently true under \(W^k_\textit{KB}\). Thus, \(a \in T_\textit{KB}(W^k_\textit{KB})\).

   If \(D\) appears negatively in rule body, the proof is similar because, given a partial interpretation \(S\), \(\lnot D\) is persistently true under \(S\) iff \(D\) is persistently false under \(S\), and we just need to swap well-founded and unfounded in the argument above.

2. (ii)

   To prove (6), assume that \(a \in U_{\pi (\textit{KB})} (W^k_{\pi (\textit{KB})}) |_\tau \) and we show \(a \in U_\textit{KB}(W^k_\textit{KB})\). Consider the case of (7). WLOG, assume that \(r\) is the only rule in \(P\) with \(a\) in the head. If the fact \(a \in U_{\pi (\textit{KB})} (W^k_{\pi (\textit{KB})})\) is independent of \(\bar{p_j}(\mathbf{e})\), the proof is trivial. Otherwise, that \(a \in U_{\pi (\textit{KB})} (W^k_{\pi (\textit{KB})})\) is because \(D'\) is persistently false under \(\lnot . U' \cup W^k_{\pi (\textit{KB})}\), where \(U'\) is the greatest unfounded set relative to \(W^k_{\pi (\textit{KB})}\). This implies that \(\bar{p_j}(\mathbf{e})\) must be unfounded w.r.t. \(W^k_{\pi (\textit{KB})}\), and it follows that \(p_j(\mathbf{e})\) is well-founded already w.r.t. \(W^{k'}_{\pi (\textit{KB})}\), for some \(k' < k\). Then, by induction hypothesis, we have that \(p_j(\mathbf{e})\) is well-founded w.r.t. \(W^k_\textit{KB}\), which implies that \(B(r)\) is persistently false under \(\lnot . U \cup W^k_\textit{KB}\), where \(U\) is the greatest unfounded set w.r.t. \(W^k_\textit{KB}\). It follows \(a \in U_\textit{KB}(W^k_\textit{KB})\). The proof for the case where a dl-atom appears negatively in rule body is similar.

Hence, the proof is completed. \(\square \)

Reprints and permissions

© 2015 Springer International Publishing Switzerland

Policies and ethics