An Entailment Procedure for Kleene Answer Set Programs

Abstract

Classical Answer Set Programming is a widely known knowledge representation framework based on the logic programming paradigm that has been extensively studied in the past decades. Semantic theories for classical answer sets are implicitly three-valued in nature, yet with few exceptions, computing classical answer sets is based on translations into classical logic and the use of SAT solving techniques. In this paper, we introduce a variation of Kleene three-valued logic with strong connectives, ${\text {R}_3}$, and then provide a sound and complete proof procedure for ${\text {R}_3}$ based on the use of signed tableaux. We then define a restriction on the syntax of ${\text {R}_3}$ to characterize Kleene ASPs. Strongly-supported models, which are a subset of ${\text {R}_3}$ models are then defined to characterize the semantics of Kleene ASPs. A filtering technique on tableaux for ${\text {R}_3}$ is then introduced which provides a sound and complete tableau-based proof technique for Kleene ASPs. We then show a translation and semantic correspondence between Classical ASPs and Kleene ASPs, where answer sets for normal classical ASPs are equivalent to strongly-supported models. This implies that the proof technique introduced can be used for classical normal ASPs as well as Kleene ASPs. The relation between non-normal classical and Kleene ASPs is also considered.

This work is partially supported by the Swedish Research Council (VR) Linnaeus Center CADICS, the ELLIIT network organization for Information and Communication Technology, the Swedish Foundation for Strategic Research (CUAS, SymbiCloud Project), and Vinnova NFFP6 Project 2013-01206.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Classical Answer Set Programs (ASP) [1, 3, 15–17, 22] belong to the family of rule-based logic programming languages. The semantic framework for classical ASPs is based on the use of stable model semantics. There are two characteristics intrinsically associated with the construction of stable models (answer sets) for answer set programs. Any member of an answer set is supported through facts and chains of rules and those members are in the answer set only if generated minimally in such a manner. These two characteristics, supportedness and minimality, provide the essence of answer sets. Classical ASPs allows two kinds of negation, classical or strong negation and default or weak negation. Additionally, answer sets are implicitly partial and that partiality provides epistemic overtones to the interpretation of disjunctive rules and default negation.

There has been much work in providing numerous definitions [24] of what an answer set is and then relating particular definitions to other formalisms such as Circumscription [27] or Default Logic [32]. This body of research has provided much insight into the nature of answer sets. Additionally, the relationship with other formalisms has provided a basis for algorithms that generate answer sets for classical ASPs in addition to inference procedures (for implementations see, e.g., CLASP [13], ASSAT [25], CMODELS [23], SMODELS [36], DLV [21]). The majority of these approaches often use syntactic translations and encodings of classical ASPs into a classical two-valued framework using standard model theory. The benefit is that one can appeal to the broad body of techniques from classical logic.

In this paper, we are interested in Kleene Answer Set programs (Kleene ASPs) introduced in [7]. Our approach is based on an extension of the three-valued logic with strong connectives, K$_3$, of Kleene [19], extended with an external negation connective, $\sim \!\,$, characterizing default negation and an implication connective, $\rightarrow _s$, suitable for Kleene ASPs. This logic, which we call ${\text {R}_3}$, has been considered in [7]. Kleene ASPs are directly represented as a fragment of the ${\text {R}_3}$ language. The semantics of Kleene ASPs is based on the use of strongly supported models which turn out to be a subset of the ${\text {R}_3}$ models. It was stated previously that the intuitions behind classical ASP semantics are based on supportedness and minimality. One of the purposes in introducing Kleene ASPs and strongly supported models is to provide a weaker interpretation of non-normal ASPs where the minimality assumption on disjunction is relaxed. Separation of supportedness and minimality technically turns out to have complexity advantages when dealing with non-normal Kleene ASPs. As a derivative of this work, it can be shown that there is an equivalence between the strongly supported models of a normal Kleene ASP and the answer sets of a normal classical ASP. Consequently, these proof techniques may also be of wider interest.

The following are the main results in this paper:¹

• We present a semantic tableaux procedure for ${\text {R}_3}$ based on the use of signed formulas that is both sound and complete for ${\text {R}_3}$. It can be used both for model generation and entailment.

• The general tableaux procedure for ${\text {R}_3}$ is only sound for Kleene ASPs. For completeness, the following method is proposed:

  A filtering procedure on tableaux branches is introduced based on the definition of strong supportedness. For both normal and non-normal Kleene ASPs, the filtering procedure is shown to be sound and complete. For normal ASP$^{K}$ s it is tractable and for non-normal ones it is in $\varPi ^P_1$.

• Due to the equivalence between strongly supported models for a normal Kleene ASP and answer sets for its corresponding normal classical ASP, the proof techniques proposed here can be used directly for normal classical ASPs. Since classical answer sets are strongly supported, the proposed proof techniques remain sound for disjunctive classical ASPs.

Structure of the Paper. The paper is structured as follows. In Sect. 2 the augmented Kleene three-valued logic, ${\text {R}_3}$, is specified. Section 3 presents the general tableaux procedure for ${\text {R}_3}$. Section 4 is devoted to Kleene ASPs and its relation to classical ASPs. It is assumed the reader is familiar with classical ASP definitions (see, e.g., [24]). In Sect. 5, a sound and complete entailment procedure for Kleene ASPs, using semantic tableaux and filtering, is presented. Section 6 concludes with related work and conclusions.

2 Three-Valued Logic ${\text {R}_3}$

The basis for our approach begins with the three-valued logic with strong connectives, K$_3$, of Kleene [19], extended with an external negation connective, $\sim \!\,$, characterizing default negation.² We assume that constants T (true), F (false), U (unknown) are part of the language. The implication connective, $\rightarrow _s\,$, is defined using, $\sim \!\,$, as:³

$$\begin{aligned} A \rightarrow _sB\;=\; \sim \!A \vee \lnot \sim \!B. \end{aligned}$$

We denote this logic by ${\text {R}_3}$.

Truth tables for connectives of ${\text {R}_3}$ are shown in Table 1, where $\lnot ,\vee ,\wedge$ are the strong connectives of K$_3$, $\sim \!\,$ is the weak or external negation connective and $\rightarrow _s$ is a newly defined implication for ASP rules.

Table 1. Truth tables for ${\text {R}_3}$ connectives.

Let $\mathcal{P}$ be the set of propositional variables. By a valuation of propositional variables we understand a mapping $\mathcal{P}\longrightarrow \{\text {T},\text {U},\text {F} \}$. If A is an ${\text {R}_3}$ formula and v is a valuation then the truth value of a formula, denoted by v(A), is defined inductively extending v by using the semantics of the connectives provided in Table 1.

By a positive literal (or an atom) we mean any propositional variable of $\mathcal{P}$. A negative literal is an expression of the form $\lnot r$, where $r\in \mathcal{P}$. A (classical) literal is a positive or a negative literal. For a literal $\ell =\lnot p$, by $\lnot \ell$ we understand p. A set of literals is consistent when it does not contain a propositional variable together with its negation. An interpretation is any consistent set of literals.

Any interpretation I defines a three-valued valuation $v_I$ by:

$$\begin{aligned} v_I(p)\mathop {=}\limits ^{\mathrm {def}}\left\{ \begin{array}{ll} \text {T} &{} \text {when}\ p\in I;\\ \text {F} &{} \text {when}\ \lnot p\in I;\\ \text {U} &{} \text {otherwise}. \end{array} \right. \end{aligned}$$

(1)

Also, given v, one can construct a corresponding interpretation $I_v$ by setting:

$$\begin{aligned} I_v\mathop {=}\limits ^{\mathrm {def}}\{p\mid p\in \mathcal{P}\ \text {and}\ v(p)=\text {T} \}\cup \{\lnot p\mid p\in \mathcal{P}\ \text {and}\ v(p)=\text {F} \}. \end{aligned}$$

(2)

In the rest of the paper, we will freely switch between interpretations and valuations, using (1) and (2).

An interpretation I is a model of a set of formulas S iff for all $A\in S$, $v_I(A)=\text {T}$, where $v_I$ is the valuation corresponding to I.

By convention, the empty conjunction is T and the empty disjunction is F.

3 Signed Tableaux for Three-Valued Logic ${\text {R}_3}$

We follow the signed tableaux style of [6], extended with rules for $\rightarrow _s$.⁴ The generalization to multivalued logics is derived from [37].

By an information constraint lattice we mean the lattice $L\mathop {=}\limits ^{\mathrm {def}}\langle \mathcal {S}; \sqcup , \sqcap \rangle$ where:

• $\mathcal {S} = \{ [\text {T} ], [\text {F} ], [\text {U} \, \text {F} \, \text {T} ], [\text {U} \, \text {T} ], [\text {U} \, \text {F} ], [\text {U} ], [\ ] \}$ is the set of signs which also contains the element $[\ ]$, representing contradiction; moving upwards in the lattice should be interpreted as tightening for possible truth values for a formula;

• $\sqcup$ ($\sqcap$) are the join (meet) operation on $\mathcal {S}$ defined respectively as the least upper bound and greatest lower bound w.r.t. the ordering shown in Fig. 1.

Fig. 1.

Information constraint lattice.

A signed formula is any expression of the form $[s]A$, where $[s]\in \mathcal {S}$ in the lattice L. A valuation u satisfies a signed formula $[a\ldots b]A$ if it satisfies the disjunction:

$$\begin{aligned} u(A)= a\,\mathrm {or}\,\ldots \,\text {or}\ u(A)= b, \end{aligned}$$

(3)

where “or” in (3) is the classical disjunction.

A valuation u satisfies a set of signed formulas S iff u satisfies every formula in S. An interpretation is a model of S iff the corresponding valuation satisfies S.

3.1 Tableaux Construction Rules

Tableaux [37] are used to construct models for formulas. The construction of a tableau starts with a formula for which models (if any) are constructed. The tableau is then expanded according to rules provided in the subsequent subsections. The following types of rules are used, where ‘,’ and ‘|’ represent conjunction and disjunction, respectively:

Table 2. Tableaux rules.

The following theorem can be proved extending the corresponding proof for K$_3$ given in [6] by considering the new connective $\rightarrow _s$.

Theorem 1

Tableau rules shown in Table 2 are sound and complete for ${\text {R}_3}$, i.e., a formula A is unsatisfiable iff there is a closed tableau for A.   $\lhd$

3.2 Constructing Models Using Tableaux

A path in a tableau is completed if no tableau rule can extend the path. A tableau is completed when all its paths are completed.

Let $[s]A$ and $[s']A$ be signed formulas. A path in a tableau is closed if both $[s]A$ and $[s']A$ are in the path and $[s]\sqcup [s'] = [\ ]$. A path is open when it is not closed.

A tableau $\mathcal T$ is closed if all its branches are closed. A tableau is open if it is not closed.

Given a tableau $\mathcal T$ for a formula A, to extract u satisfying A we look for an open branch. If such a branch does not exist then there is no model for A. Otherwise, for each propositional variable p appearing in the branch let:

$$\begin{aligned} \varSigma (p)\mathop {=}\limits ^{\mathrm {def}}\{s\mid [s]p\ \text {occurs in the branch}\} \ \text {and let}\ \sigma (p)\mathop {=}\limits ^{\mathrm {def}}\bigsqcup _{s\in \varSigma (p)}\!\![s]. \end{aligned}$$

The satisfying valuations (models) are then defined by assigning, to each p occurring in the branch, a value from $\sigma (p)$. If for a propositional variable p, occurring in A, no formula of the form $[s]p$ occurs on a given branch then p is unconstrained and can be assigned any truth value. Note that, due to the form of rules, only signs [F], [T], [U F] and [U T] can appear in tableaux. If a proposition p does not occur in a branch, we assume that implicitly $[\text {U} \,\text {F} \,\text {T} ]p$ occurs in that branch.

Example 1

Consider the following tableau:

The first branch contains $[\text {U} \,\text {F} ]q$ and $[\text {T} ]p$, so $\sigma (q)=[\text {U} \,\text {F} ]$ and $\sigma (p)=[\text {T} ]$. The branch then encodes two models:

$$\begin{aligned} v_1(q)= & {} \text {U}, v_1(p)=\text {T},\ \text {corresponding to}\ \{p\},\\ v_2(q)= & {} \text {F}, v_2(p)=\text {T},\ \text {corresponding to}\ \{\lnot q, p\}. \end{aligned}$$

The second branch contains $[\text {U} \,\text {F} ]q$ and $[\text {F} ]q$, so $\sigma (q)=\text {F}$. Since p remains unconstrained, the branch encodes models:

$$\begin{aligned} u_1(q)= & {} \text {F}, u_1(p)=\text {T}, \ \text {corresponding to}\ \{\lnot q, p\},\\ u_2(q)= & {} \text {F}, u_2(p)=\text {F}, \ \text {corresponding to}\ \{\lnot q, \lnot p\},\\ u_3(q)= & {} \text {F}, u_3(p)=\text {U},\ \text {corresponding to}\ \{\lnot q\}. \end{aligned}$$

Of course, $v_1, v_2, u_1, u_2, u_3$ are all models for the starting formula $(p\vee \lnot q)\wedge \sim \!q$.

   $\lhd$

We have the following theorem which can be proved by extending the proof of the analogous theorem for K$_3$ given in [6].

Theorem 2

Given an ${\text {R}_3}$ formula A, every interpretation satisfying A can be extracted from a completed tableau for $[\text {T} ]A$.   $\lhd$

4 (Kleene) Answer Set Programs

The syntax for Kleene Answer Set Programs, ASP$^{K}$, is identical for that of classical ASP programs. The semantics for Kleene ASP$^{K}$ programs is based on the use of the augmented three-valued Kleene logic $R_3$ and strongly-supported models presented in [7]. The semantics for classical ASP programs is based on stable model semantics [24]. Correspondences between classical answer sets and strongly supported models will be considered later in this section. For the sake of clarity we consider propositional programs only.

By an ASP$^{K}$ rule we understand an expression $\varrho$ of the form:

$$\begin{aligned} \ell _1\vee \ldots \vee \ell _k\leftarrow \ell _{k+1},\ldots ,\ell _m, not \,\ell _{m+1},\ldots , not \,\ell _n, \end{aligned}$$

(4)

where $n\ge m\ge k\ge 0$ and $\ell _1,\ldots ,\ell _k,\ell _{k+1},\ldots , \ell _m, \ell _{m+1},\ldots \ell _n$ are (positive or negative) literals. The expression at the lefthand side of ‘$\leftarrow$ ’ in (4) is called the head and the righthand side of ‘$\leftarrow$’ is called the body of the rule. The rule is called disjunctive if $k>1$.

An ASP$^{K}$ program $\varPi$ is a finite set of rules. A program is normal if each of its rules has at most one literal in its head. If a program contains a disjunctive rule, we call it disjunctive or non-normal.

An interpretation I satisfies a rule $\varrho$ of the form (4), denoted by $I\,\models \,\varrho$, if whenever $\ell _{k+1},\ldots , \ell _m\in I$ and $\ell _{m+1},\ldots , \ell _n\not \in I$, we have $\ell _i\in I$ for some $1\le i\le k$. An interpretation I satisfies an ASP$^{K}$ program $\varPi$, denoted by $I\,\models \, \varPi$, if for all rules $\varrho \in \varPi$, $I\,\models \,\varrho$.

We say that an Kleene ASP program $\varPi$ entails an ${\text {R}_3}$ formula A, and denote it by $\varPi \,\models \, A$, provided that A is true in every strongly supported model of $\varPi$.

The concept of strong supportedness [7] builds on the principle of constructing models through chains of rules grounded in facts. When evaluating the body of a rule to determine whether it is applicable, literals outside the scope of $not \,$ must be evaluated against the set of literals for which support has already been found, represented as an interpretation I. However, literals inside the scope of $not \,$ must be evaluated against a strongly supported model candidate J, similarly to how $not \,\ell$ is evaluated against an answer set candidate S when a reduct $\varPi ^S$ is computed classically. We therefore evaluate formulas w.r.t. two interpretations. Given interpretations I and J, the value of a formula A w.r.t. (I, J), denoted by (I, J)(A), is defined as follows:

$$\begin{aligned} (I,J)(A)\mathop {=}\limits ^{\mathrm {def}}\left\{ \begin{array}{ll} \text {T} &{} \text {when}\ I\,\models \, reduct^J(A);\\ \text {F} &{} \text {when}\ I\,\models \, reduct^J(\lnot A);\\ \text {U} &{} \text {otherwise}. \end{array} \right. \end{aligned}$$

(5)

where $reduct^J(A)$ (respectively, $reduct^J(\lnot A)$) is a formula obtained from A ($\lnot A$) by substituting subformulas of the form $not \,\ell$ by their truth values evaluated in J.

Now we are ready to define strong supportedness. An interpretation N is a strongly supported model of an ASP$^{K}$ program $\varPi$ provided that N satisfies $\varPi$ and there exists a sequence of interpretations $I_0\subseteq I_1\subseteq \ldots \subseteq I_n$ where $n\ge 0$ such that $I_0=\emptyset$, $N=I_n$, and:

• 1. for every $1\le i\le n$ and every rule $\ell _1\vee \ldots \vee \ell _k\leftarrow B$ of $\varPi$,

  if $\big (I_{i-1},N\big )(B)=\text {T}$ then a nonempty subset of $\{\ell _1,\ldots ,\ell _k\}$ is included in $I_i$;

• 2. for $i=1,\ldots ,n$, $I_i$ can only contain literals obtained by applying point 1.

A Kleene Answer Set for an ASP$^{K}$ program is a strongly supported model. The terminology will be used interchangeably.

The following correspondences between classical answer sets with stable model semantics (for definitions see, e.g., [24]) and Kleene answer sets with strongly-supported model semantics relate the two semantics.

In [7] the following theorem is proved (see [7, point 2 of Theorem 1]).

Theorem 3

For any normal ASP$^{K}$ program $\varPi$, I is a classical answer set of $\varPi$ iff I is a strongly supported model of $\varPi$.    $\lhd$

The following theorem clarifies the role of strong supportedness in the context of disjunctive programs.

Theorem 4

For any ASP$^{K}$ program $\varPi$, if I is a classical answer set of $\varPi$ then I is a strongly supported model of $\varPi$.    $\lhd$

Theorem 3 allows us to use the filter-based tableau technique introduced in Sect. 5 below, not only for Kleene ASPs, but for classical normal ASPs, too. Theorem 4 shows that filtering remains sound for disjunctive classical ASPs.⁵

5 Filtering Technique for Kleene Answer Set Programs

To construct tableaux for Kleene ASP entailment we first translate Kleene ASPs into formulas of ${\text {R}_3}$ using the translation Tr defined as follows:

$$\begin{aligned}&Tr(\lnot A)\mathop {=}\limits ^{\mathrm {def}}\lnot A, \;Tr( not \,A)\mathop {=}\limits ^{\mathrm {def}}\sim \!A,\nonumber \\&Tr(A\circ B)\mathop {=}\limits ^{\mathrm {def}}Tr(A)\circ Tr(B), \text {for}\ \circ \in \{\vee ,\wedge \},\nonumber \\&Tr(A\leftarrow B)\mathop {=}\limits ^{\mathrm {def}}Tr(B)\rightarrow _sTr(A). \end{aligned}$$

(6)

Rules are then translated as follows:

$$\begin{aligned}&Tr(\ell _0 \vee \ldots \vee \ell _i \leftarrow \ell _{i+1},\ldots , \ell _j, not \,\ell _{j+1}, \ldots , not \,\ell _m)=\nonumber \\&\qquad (\ell _{i+1}\wedge \ldots \wedge \ell _j\wedge \sim \!\ell _{j+1}\wedge \ldots \wedge \sim \!\ell _m)\rightarrow _s(\ell _0 \vee \ldots \vee \ell _i). \end{aligned}$$

(7)

For a Kleene ASP program $\varPi$, $Tr(\varPi )\mathop {=}\limits ^{\mathrm {def}}\bigwedge _{r\in \varPi }Tr(r)$. By a model of a Kleene ASP program $\varPi$ we understand any model of $Tr(\varPi )$.

Note that every Kleene answer set for a program $\varPi$ is an ${\text {R}_3}$ model for $Tr(\varPi )$. Therefore, we have the following theorem.

Theorem 5

Let $\varPi$ be a Kleene ASP program, A be an ${\text {R}_3}$ formula, and $\mathcal T$ be a tableau for:

$$\begin{aligned}{}[\text {T} ]\big (Tr(\varPi )\, \wedge \! \sim \!A\big ). \end{aligned}$$

(8)

Then, if $\mathcal T$ is closed then $\varPi \,\models \, A$.   $\lhd$

That is, the tableaux procedure provided in Sect. 3.1 is sound for Kleene ASP entailment.

Example 2

Let $\varPi$ consists of rules:

$$\begin{aligned}&q\leftarrow p.\\&q\leftarrow not \,p. \end{aligned}$$

To show that $\varPi \,\models \, q$ we construct the following tableau:

On the first branch $\sigma (p)=[\ ]$ and on the other two branches $\sigma (q)=[\ ]$. Thus the above tableau is closed.   $\lhd$

For completeness of ASP$^{K}$ , a filtering technique is required to filter out non-strongly supported models associated with open branches. To decide whether $\varPi \,\models \, A$ we first construct a tableau $\mathcal T$ for signed formula (8). Then,

• 1. if $\mathcal T$ is closed then $\varPi \,\models \, A$; otherwise

• 2. filtering: eliminate every open branch of $\mathcal T$ encoding only non-strongly supported models of $\varPi$. If all open branches of $\mathcal T$ are eliminated then $\varPi \,\models \, A$, otherwise $\varPi \not \,\models \, A$.

The filtering described in point 2. Above is sound and complete for ASP$^{K}$, as stated in the following theorem.

Theorem 6

Let $\varPi$ be a Kleene ASP program, A be an ${\text {R}_3}$ formula, and $\mathcal T$ be a tableau for $[\text {T} ]\big (Tr(\varPi )\wedge \sim \!A\big )$. Then, $\varPi \!\,\models \,\! A$ iff filtering eliminates every open branch of $\mathcal T$.   $\lhd$

Example 3

Let program $\varPi$ consist of a single rule: $q\leftarrow not \,p$. To show that $\varPi \,\models \, q$, we construct the following tableau:

The first branch is open and the second branch is closed. Therefore we have to check whether the first branch represents a strongly supported model for $\varPi$. Since the branch contains $[\text {U} \,\text {F} ] q$ and $[\text {T} ]p$, the candidates for a strongly supported model for $\varPi$ are $\{p\}$ and $\{\lnot q, p\}$.⁶ Of course, $\{p\}$ and $\{\lnot q, p\}$ are not strongly supported, so there are no open branches representing strongly supported models for $\varPi$. Therefore, $\varPi$ indeed entails q.    $\lhd$

For non-normal programs an open branch may encode more than one strongly supported model, consequently the technique shown in Example 3 does not apply since one uses an assumption of equivalence between minimality and strong supportedness that only applies to normal programs. In this case one is required to filter all potential interpretations, including non-minimal ones, associated with an open branch.

To verify strong supportedness one can use Algorithm 1 provided in [7, p. 137]. Given a program $\varPi$ and an interpretation I, this algorithm checks whether I is a strongly supported model of $\varPi$ in deterministic polynomial time w.r.t. $\varPi$ and I. Recall that due to the form of tableau rules shown in Table 2, only signs [F], [T], [U F] and [U T] (and implicitly [U F T]) can appear in tableaux. Therefore, to check whether a given open branch of a tableau encodes a strongly supported model, one can extract the candidate valuation v in such a way that whenever for a given proposition p, U is in $\sigma (p)$, we set $v(p)\mathop {=}\limits ^{\mathrm {def}}\text {U}$, otherwise v(p) is the (uniquely determined) truth value from $\sigma (p)$. That way, for normal programs, v represents a minimal interpretation uniquely determined by this branch. By Theorem 3, for normal programs strong supportedness is equivalent to minimality, so we have the following theorem.

Theorem 7

For any normal ASP$^{K}$ program $\varPi$ checking whether a given tableau branch for $[\text {T} ]\varPi$ encodes a strongly supported model is tractable.   $\lhd$

For non-normal programs, checking whether an open branch exists such that there is a valuation encoded by the branch defining a strongly supported model, is obviously in $\varSigma ^P_1$. Therefore, checking whether a branch can be closed via filtering (does not encode a strongly supported model), is in $\varPi ^P_1$ (i.e., co-NP) as stated in the following theorem.

Theorem 8

For any non-normal ASP$^{K}$ program $\varPi$ checking, in general, whether a given tableau branch for $[\text {T} ]\varPi$ encodes a strongly supported model, is in $\varPi ^P_1$.   $\lhd$

Note that Theorem 8, ensures that our entailment procedure is in $\varPi ^P_1$.

Remark 1

The technique of filtering can be applied to classical answer sets, too. First, one can filter out non-strongly supported models. This can be done “locally” node by node. Normal classical ASP programs are equivalent to normal ASP$^{K}$ programs so for this case our procedure remains sound and complete. For non-normal classical ASP programs, the minimality requirement results in a higher complexity of reasoning [8, 9], [7, Thm. 2, p. 137] (assuming that the polynomial hierarchy does not collapse). In this case, checking for non-minimality rather than for non-supportedness is required. It calls for pairwise comparisons with all models, perhaps encoded by other nodes in the constructed tableaux. Therefore, rather than checking for minimality, we could achieve completeness for non-normal classical ASPs by suitably adding a generalization of Clark’s completion and loop formulas provided in [25] to the original ASP program.   $\lhd$

6 Related Work and Conclusions

There is a rich history of explicit use of partial interpretations and multi-valued logics as a basis for semantic theories for logic programs. Some related and additional representative examples are [5, 11, 12, 20, 30, 31, 34, 38]. Supportedness is analyzed in many papers, starting from [10]. One of most recent generalizations, via grounded fixpoints, is investigated in [2]. However, grounded fixpoints are minimal (see [2, Proposition 3.8]) while strongly supported models do not have to be minimal.

In [33] a possible model semantics for disjunctive programs is proposed. It is formulated with the use of split programs and there can be exponentially many of them comparing to the original program. Similar semantics was independently proposed in [4] under the name of the possible world semantics. In comparison to [33], ASP$^{K}$ programs allow for strong negation and a three-valued model-theoretic semantics is provided. The presence of both default and strong negation in ASP$^{K}$ provides a tool to close the world locally in a contextual manner, more flexible than possible model negation proposed in [33]. Though defined independently and using different foundations, both semantics appear compatible on positive programs, so the results of the current paper apply to possible model semantics of [33], too.

Paper [14] defines a tableaux framework for classical ASP, using two (explicit) truth values T, F. They require a cut rule, whereas we do not. Loop formulas are explicit in some rules and supportedness is encoded as an additional set of inference rules. Our approach is very much in the spirit of Smullyan [37] and does not require special inference rules, although loop and completion formulas would have to be added to an ASP if one wanted to deal with classical non-normal ASPs.

In [29, 30], the logic of here-and-there (HT) is used to define a direct declarative semantics for classical ASPs, although HT has greater generality and wider application. HT can be defined by means of a five-valued logic, N$_5$, defined over two worlds: h (here) and t (there), where the set of literals associated with h is included in the set of literals associated with t. N$_5$ uses truth values $\{-2,-1,0,1,2\}$, where the values $-1, 1$ characterize literals associated with h and not associated with t. On the other hand, for classical ASP models it is assumed that these sets are equal, so $-1,1$ become redundant. Therefore, in the context of classical ASPs one actually does not have to use full N$_5$ as it reduces to the three-valued logic ${\text {R}_3}$, with $-2, 0, 2$ of N$_5$ corresponding to F, U, T of ${\text {R}_3}$, respectively. Consequently, tableaux techniques used in [29] for N$_5$ could then be simplified when focus is on ASPs.

Kleene Answer set programs, ASP$^{K}$, and connectives used in ${\text {R}_3}$ have been proposed in [7]. The current paper introduces a sound and complete tableaux-based proof procedure for them. A filtering technique is introduced which, when added to the ${\text {R}_3}$ tableaux based proof procedure, provides a sound and complete proof procedure for Kleene ASPs. As a derivative result, it is shown that the proof procedure is also sound and complete for classical normal ASPs and remains sound for disjunctive classical ASPs.