A Rational Extension of Stable Model Semantics to the Full Propositional Language

1 Introduction

Answer set programs constitute one of the most important declarative programming paradigms that are readily available and actively being expanded. Stable model semantics is the semantics behind the success of answer set programming. Stable model semantics is proven to be suitable for declarative specification of many tasks, specifically those that require non-monotonic reasoning or reasoning about beliefs of agents. Due to this success, there has been many efforts to extend this semantics to a more general class of programs (i.e., to lift the restriction on answer set programs to have the form of either a normal or a disjunctive logic program). Such efforts mainly fall into two categories: (1) those with a practical goal to extend the language of answer set programs with specific constructs such as aggregates, and, (2) those with a fundamental approach that bring new insights into the stable models themselves.

This paper falls into the second category above because we are not motivated by a particular construct for which a semantics is needed. Instead, what motivates us is a combination of the following: (1) pure interest in the philosophy of stable models, (2) practical need to extend stable models to the full propositional language, and, (3) the current shortcomings of existing extensions of stable model semantics.

We believe that the main philosophical principle behind the development of stable models (and the reason for its success) is the principle of rationality: all atoms in all stable models are justified and justifications are well-founded (not circular). This principle is sometimes known as the property of being strongly grounded and is, of course, useful when modeling the set of possible belief sets of rational agents. It was first noted in [Moore, 1985] that one of the places where non-monotonic reasoning excels is to model the process of reasoning about knowledge and, thus, autoepistemic reasoning was introduced. Later, in their seminal paper introducing stable model semantics, Gelfond and Lifschitz [Gelfond and Lifschitz, 1990] noted that stable models also serve the same purpose. Therefore, we expect extensions of stable model semantics to also adhere to the same philosophical principle and disallow self-justified models.

As we see in Examples 1 and 2, neither of the two main extensions of stable model semantics (i.e., equilibriummodel semantics [Pearce, 2006] and FLP semantics [Faber et al., 2004]) guarantee this desired property. Our examples demonstrate cases where FLP semantics and equilibrium models do not agree. We argue that, in the first case, the natural interpretation is the one given by FLP semantics, while, in the second case, equilibriummodels give the more natural interpretation. The main achievement of this paper is to define a new extension of stable model semantics that works flawlessly in all cases.

Example 1. Consider programΠ1 as follows:

Π1 is neither a normal nor a disjunctive logic program (because of "not not b" in the body of its first rule). Thus, stable model semantics is not applicable to Π1. However, both equilibrium model semantics and FLP semantics are applicable to Π1. Both these semantics agree that Π1 has an intended model S1 := ∅ but, according to equilibrium models, Π1 has yet another intended model S2 := {a, b}. We want to argue that S2 suffers from self-justification and, hence, is not rational.

Equilibrium model S2 asserts that both a and b are believed so they should both be justified. However, according to Π1, the only possible justification for a is "not not b". Thus, not not b should be believed and its justification should not depend on a (otherwise, it would constitute a selfjustification). To believe in "not not b", not b should not be believable, i.e., every way to believe in b should fail. Now, since the only way to believe b is to first believe in a and since this only way constitutes a self-justification, b cannot be believed. Thus, we cannot believe in "not not b" and, hence, we cannot believe in a either. The following self-justified chain summarizes our discussion:

Above argument shows that S2 is self-justified (also sometimes known as circularly justified) and it should not be an intended model of Π1. Thus, a a faithful extension of stable model semantics can only allow S1. So, in this example, FLP semantics works as desired and captures the right model. Equilibrium model semantics, on the other hand, allows nonintended models.

Before moving on, consider normal logic program Π′1 := {a ← not c. , b ← a. , c ← not b.}. Stable models of Π′1 are S′1 := {c} and S′2 := {a, b}. We like to point out that, in Π′1 , model S′2 is justified because it assumes "not c" and so it can deduce a and b. In terms of program Π1, however, this is like assuming the existence of some secret way to justify not not b. Such an assumption contradicts the closed-world assumption. Hence, Π1 differs from Π′1 in that Π′1 adds a new way to justify not not b that does not exist in Π1.

Note that there are other semantics that extend stable models (such as Ferraris [Ferraris, 2005]) that agree with equilibrium models over the class of propositional programs. Clearly, such semantics also allow self-justification in program Π1 of Example 1. Our next example discusses a case where FLP semantics allows self-justification while equilibrium models disallow it:

Example 2. Consider programΠ2 as follows:

Since program Π2 is not in the recognized syntax of the original definition of FLP semantics, in this example, we consider an extension of FLP semantics defined in [Truszczy´nski, 2010]. In Section 4, we consider yet another (but different) extension of FLP semantics.

According to [Truszczy´nski, 2010], Π2 has a single intended model T := {a, b}. However, according to Π2, the only possible justification for atom a is atom b. Also, atom b can only be justified by formula "a ∨ not a". However, since "not a" is not true in model T , the only possible justification for "a ∨ not a" is a itself. Therefore, model T suffers from the following self-justified chain:

Hence, we believe that T cannot be an intended model of Π2 and that Π2 should not have any intended models. This view agrees with the interpretation given by equilibrium models for Π2. Thus, in this example, equilibrium model semantics captures the right intended models while FLP semantics allows self-justification.

Examples 1 and 2 show that neither equilibrium model semantics nor FLP semantics do not capture the right intended models everywhere. This paper extends stable model semantics in a way that is faithful to its founding principle of only allowing rational belief sets. Our semantics has the following properties:

1. It is defined for full propositional language,
2. It extends stable model semantics, and,
3. It represents the possible belief sets of a rational agent, i.e., all beliefs are justified and self-justifications are disallowed.

The semantics we propose is based on intuitionistic derivability and, thus, it enables us to use the full force of intuitionistic logic to study stable models.

In what follows, Section 2 reviews the necessary background. Section 3 introduces supported model semantics and gives a proof that supported model semantics indeed extends stable model semantics (i.e., on the class of normal/disjunctive logic programs, they coincide). Section 3 also gives an important characterization of supported models in terms of Kripke structures. Section 4 relates our semantics to other non-monotonic semantics. We prove that all supported models are minimal classical models, Clark completion models, and, most importantly, equilibrium models (note that the other direction does not hold in general). Finally, Section 5 characterizes the complexity of different reasoning tasks in supported model semantics. Our results show that such tasks remain as computationally complex as similar tasks in other extensions of stable model semantics.

2 Background

Here, we review the required background of this paper. Logic programs are sets of rules r of form:

where 0 ≤ i ≤ n. h1, · · · , hm are propositional atoms called heads of r and p1, · · · , pn are propositional atoms forming the body of r. A rule r is (a) normal if m = 1, (b) disjunctive if m > 1, and, (c) a constraint if m = 0. Normal logic programs (NLP) can only have normal rules but disjunctive logic programs (DLP) can have both normal and disjunctive rules. A constraint can be expressed using normal rules and, thus, can be included in both NLPs and DLPs. The intuitive reading of Rule (3) is that if all atoms p1, · · · , pi are believed and none of the atoms pi+1, · · · , pn can be believed, then there is a reason to believe at least one of the atoms h1, · · · , hm.

Propositional programs are sets of arbitrary propositional formulas. A propositional formula is a formula constructed using propositional atoms a, b, c, · · · , binary operators ∧, ∨ and →, and zero-ary constant ⊥. The propositional formula representing Rule (3) is:

We also use operators ←, ¬ and not as syntactical variants of →, i.e., (φ ← ψ) := (ψ → φ) and (not φ) := ¬φ := φ → ⊥. Moreover, we define ⊤ := (⊥ → ⊥) and ¬.A := {¬a | a ∈ A} (A is a set of propositional atoms). Furthermore, for propositional programΠ, vocab(Π) denotes the set of all propositional atoms used in Π.

Example 3. Propositional programs Π1 and Π2 from Examples 1 and 2 can be represented as follows:

Stable model semantics is a semantics for logic programs. Let Π be a DLP and S a set of propositional atoms. ΠS is the set of positive rules "h1; · · · ; hm ← p1, · · · , pi" s.t. a rule "h1; · · · ; hm ← p1, · · · , pi, not pi+1, · · · , not pn" exists in Π with S ∩ {pi+1, · · · , pn} = ∅, i.e., ΠS is the positive part of Π that remains applicable according to S. S is a stable model of Π iff S is a minimal classical model of ΠS .

Equilibriummodel semantics extends stable models to full propositional language and is defined using satisfiability in logic of here and there (HT-logic). In HT-logic, HT-model is a pair 〈H, T 〉 where H ⊆ T ⊆ U (U: the universe of propositional atoms). In HT-logic, 〈H, T〉|=HTφ if: 1. φ is a propositional atom a and a ∈ H, 2. φ := (φ1∧φ2) and 〈H, T 〉|=HTφ1 and 〈H, T 〉|=HTφ2, 3. φ := (φ1∨φ2) and either 〈H, T 〉|=HTφ1 or 〈H, T〉|=HTφ2, or, 4. φ := (φ1 → φ2) and both of the following hold: (a) if 〈H, T〉|=HTφ1 then 〈H, T〉|=HTφ2, and, (b) if 〈T, T〉|=HTφ1 then 〈T, T〉|=HTφ2. Also, for a propositional program Π, 〈H, T 〉|=HTΠ if 〈H, T 〉|=HTφ for all φ ∈ P . Finally, a set S of propositional atoms is an equilibrium model of Π if (1) 〈S, S〉|=HTΠ, and, (2) for all S′ ⊊ S: 〈S′ , S〉 ̸ |=HTΠ.

Interested reader is referred to [Apt and Bol, 1994] for a thorough review of stable models and to [Pearce, 2006] (resp. to [Faber et al., 2004]) for a detailed discussion on equilibrium models (resp. FLP semantics). Also, [Lifschitz, 2010] compactly (and usefully) reviews thirteen different ways of defining stable models.

Intuitionistic logic is a subset of classical logic without the law of excluded middle. Here, ConI(Γ) (resp. Con(Γ)) denotes intuitionistic (resp. classical) consequences of Γ.

3 SupportedModels

This section introduces the notion of supported models in terms of a form of completion in intuitionistic logic. We start by a simple definition of intended models (that we call supported models) and, thanks to the vast literature on intuitionistic logic, we are able to characterize supported models in terms of Kripke models. The latter characterization is extremely useful when we relate supported models to other non-monotonic semantics.

Definition 1 (SupportedModels). Let Π be a propositional program and let U be the universe of propositions (particularly, vocab(Π) ⊆ U). Then, for S ⊆ U, we say that S is a supported model of Π w.r.t. universe U iff (1) ⊥ ̸∈ ConI (Π ∪ ¬.(U \ S)), and, (2) S ⊆ ConI (Π ∪ ¬.(U \ S)).

The intuition behind Definition 1 is that a model S is supported in a program Π if the justification for inclusion of all propositions asserted by S can be traced back to one of the following primitive justifications (without circularity):

1. Something that is intuitionistically trivial,
2. Something that is asserted by Π, or,
3. Nonbelief in a propositional atom.

The inclusion of the last primitive justification above is motivated by the closed-world assumption and the innate justification it brings for nonbelief in a propositional atom. Moreover, it is also a widely accepted philosophical principle that the burden of proof can only be expected for propositions that are asserted, i.e., propositional atoms in S. Thus, Definition 1 says that a model is supported if, firstly, nonbelief in excluded atoms does not make us inconsistent and, secondly, included atoms are justified (without circularity) by the program Π and nonbelief in excluded atoms. Non-circularity of justifications in Definition 1 is guaranteed by the well-founded-ness and finiteness of their intuitionistic proofs.

Example 4. Consider program Π1 of Example 1. Firstly, S1 = ∅ is supported because Π1 ∪ {¬a, ¬b} is consistent. Secondly, S2 = {a, b} is not supported because a ̸∈ ConI (Π1).

Similarly, consider program Π2 of Example 2. Model T = {a, b} is not supported because a, b ̸∈ ConI(Π2) (note that a and b are classically derivable from Π2). Intuitionistic underivability of a and b is shown using HT-model 〈∅, {a, b}〉 that satisfies Π2 but not a or b.

We now want to prove that supported models extend stable models, but we first need a lemma and a definition:

Lemma 1. For positive DLP Π (i.e., Π has no negative literal in the body of its rules) and universe U of propositional atoms, we have that for all S ⊆ U, S is supported in Π iff S is a minimal classical model of Π.

Proof. Define Π′ := Π∪¬.(U \ S). (⇒) By S being a supported model of Π, we know S ⊆ ConI(Π′ ) ⊆ Con(Π′ ). Also, since ⊥ ∈ ConI(Γ) iff ⊥ ∈ Con(Γ) (for any propositional theory Γ [Kleene, 1952]), we know that Π is classically satisfiable. Therefore, S is a minimal classical model of Π.

(⇐) Let S be a minimal classical model of Π. Since equilibrium models agree with stable models on DLPs, S is an equilibrium model of Π too. Now, assume that S is not supported. Then, there exists a Kripke model 〈K, α〉 s.t. α⊩Π′ but α ̸ ⊩S. Since S is a minimal classical model of Π′ and since every β ≥ α forces Π′ , we know that, all maximal states β ≥ α force S. Now, take maximal state γ ≥ α s.t. γ ̸ ⊩S (i.e., if γ ′ > γ then γ ′⊩S). Define H := {a ∈ U | γ⊩a}. Since 〈H, S〉|=HTΠ′ and H ⊊ S, our assumption of S being an equilibrium model is contradicted. Hence, S is supported.

Definition 2 (Classical Kripke Model). Let S be a set of propositional atoms and let 〈K, α〉 with K := 〈W,≤,⊩〉, W := {α}, and ≤:= ∅ be a Kripke model such that α forces a propositional atom a if and only if a ∈ S. Then, 〈K, α〉 is known as the Kripke representation of classical model S (or, shortly, the classical Kripke model S).

Note that, for all classical models S, S |= Π iff the Kripke representation 〈K, α〉 of S has α⊩Π.

Theorem 1 (Stable Model = Supported Model (in LP's)). Let Π be an NLP/DLP and U be the universe of propositional atoms. Then, for S ⊆ U, S is a stable model of Π iff S is a supported model of Π w.r.t. U.

Proof. Let Π′ := Π∪¬.(U \S) and Π′′ := ΠS ∪¬.(U \S). (⇒) If S is a stable model then, firstly, S is a classical model and thus a classical Kripke model of Π. Therefore, Π′ is consistent. Secondly, by Lemma 1, we know that S is a supported model of ΠS . Therefore, S ⊆ ConI(Π′′ ) ⊆ ConI(Π′ ). Thus, S is supported.

(⇐) Let S be a supported model of Π. Then, firstly, Π′′ is consistent and thus Π′ is also consistent. Secondly, we know that under assumptions ¬.(U \ S), program Π is intuitionistically equivalent to program ΠS . Hence, S ⊆ ConI(Π′′ ) and thus a supported model of ΠS . Now, by Lemma 1, S is a minimal model of ΠS and thus a stable model of Π.

Since supported models are defined in terms of intuitionistic reasoning, the full force of intuitionistic logic can be used to study supported models. In particular, we want to characterize supported models using Kripke models of a propositional program.

Theorem 2 (Characterizing Supported Models). For propositional program Π and finite universe U of propositional atoms, we have: for all S ⊆ U, S is a supported model of Π w.r.t. U iff (1) the Kripke representation of S forces Π, and, (2) for all Kripke models 〈K, α〉 of Π ∪ ¬.(U \ S), all β ≥ α, and all a ∈ S, we have β⊩a.

Proof. (⇒) Let S be a supported model of Π. Then, Π ∪ ¬.(U \S) is consistent. Therefore, S is a classical model of Π and, thus, the Kripke representation of S forces Π. Moreover, since S ⊆ ConI (Π∪¬.(U \S)), for all Kripke models 〈K, α〉 of Π ∪ ¬.(U \ S), α⊩a. Thus, for all β ≥ α, and all a ∈ S, β⊩a.

(⇐) Let S be a classical Kripke model of Π s.t. for all Kripke models 〈K, α〉 of Π′ := Π ∪ ¬.(U \ S), all β ≥ α, and all a ∈ S, we have β⊩a. Then, S is a classical model of Π and, so, a classical model of Π′ . Thus, firstly, Π′ is consistent and, secondly, every a ∈ S is true in all Kripke models of Π′ and, hence, an intuitionistic consequence of Π′ . Therefore, S is a supported model of Π.

A nice consequence of Theorem 2 is the property that all supported models are minimal classical models:

Corollary 1 (Supported ⊆Minimal Classical). Let Π be a propositional program with finite vocabulary and let S be a supported model of Π. Then, S is a minimal classical model of Π.

Remember Example 1 from Section 1. Corollary 1 shows that, indeed, S2 is not supported (since it is not a minimal model). Moreover, Corollary 1 connects supported models to minimal classical models. Next section connects supported models to other non-monotonic semantics in a similar way.

4 Relation to Existing Non-monotonic Semantics

This section connects our supported model semantics to other frameworks for non-monotonic reasoning. Perhaps, due to the wide acceptance of FLP semantics [Faber et al., 2004] and equilibriummodel semantics [Pearce, 2006], the most important question that must be answered here is how supported models relate to these two semantics.

We first start by the relation between our supported semantics and equilibrium models. As pointed out by [Pearce, 2006], HT-logic is an intermediate logic (a logic that lies between classical and intuitionistic logic). Therefore, it is no surprise that a very natural connection exists between equilibrium models and supported models. Indeed, an HT-model is a special kind of Kripke models with only two states H and T such that H ≤ T. According to [Pearce, 2006], S is an equilibriummodel of P if 〈S, S〉|=HTP but for all S′ ⊊ S: 〈S′ , S〉 ̸ |=HTP .

So, clearly, all supported models are equilibrium models too because (1) they are classical Kripke models, and, (2) they are the only minimal Kripke models. The following Theorem states exactly this fact:

Theorem 3 (Supported Models ⊆ Equilibrium Models). For propositional program Π with finite universe, every supported model is also an equilibrium model.

Note that the inverse of Theorem 3 does not hold, i.e., there exist equilibrium models that are not supported. One such equilibriummodel is, indeed, model S2 from Example 1. Theorem 4 shows that HT-models (unlike equilibrium models) can completely characterize supportedness:

Theorem 4. For propositional program Π over a finite universe U, we have that, for every S ⊆ U, S is supported iff 〈S, S〉 is the unique HT-model of Π ∪ ¬.(U \ S).

Proof. (⇒) Let S be a supported model of Π. Then, by Corollary 1, S is a classical model of Π′ := Π ∪ ¬.(U \ S) and thus 〈S, S〉 is an HT-model of Π′ . Also, for all HT-models 〈H, T 〉 of Π′ , by Theorem 2, we have H = T = S.

(⇐) Let S be the unique HT-model of Π′ := Π ∪ ¬.(U \ S). Assume that we have a Kripke model 〈K, α〉 of Π′ , a state β ≥ α and some a ∈ S such that β ̸ ⊩a. Take maximal state γ ≥ β such that γ ̸ ⊩S (i.e., every state γ ′ > γ forces S). Define H := {a ∈ U | γ⊩a}. Now, if γ is a maximal state in K (i.e., there is no state γ ′ > γ) then consider M := 〈H,H〉 and, otherwise, consider M := 〈H, S〉. Since M|=HTΠ′ and H ⊊ S, it contradicts our assumption of 〈S, S〉 is the unique HT-model of Π′ . Therefore, by Theorem 2, S has to be supported.

Another interesting semantics for negation as failure in logic programs is given by Clark [Clark, 1977]. The Clark completion idea can be generalized to include rules with fully propositional bodies (instead of just a conjunction of literals). It so happens that supported models are also models of the Clark completion of a program, i.e., for a program Π consisting of only rules with an atom as their head, if an atom a is in a supported model S, then there should exist a rule r ∈ P

with head(r) = a such that S classically satisfies body(r). The following theorem states this fact formally:

Theorem 5 (Supported Models ⊆ Clark Completion Models). Let Π be a finite program and U a finite universe of propositional atoms. Then, all supported models of Π are also Clark completion models of Π.

Note that Theorem 5 can also be viewed as a consequence of Theorem 3 because all equilibrium models of a program are also models of its Clark completion. Indeed, the proof of Theorem 5 shows that not being a model of Clark completion guarantees the existence of a minimal Kripke model with only two states (i.e., an HT-model 〈S′ , S〉 with S′ ⊊ S) that contradicts our characterization of supported models in terms of Kripke models.

Now, let us turn to FLP semantics. The intersection of the syntax of propositional programs and the syntax for which the original FLP semantics is exactly the syntax of disjunctive logic programs. On this limited intersection of syntax, FLP semantics coincides with stable model semantics and, thus, coincides with our supported semantics. However, there are extensions of FLP semantics that generalize the idea of FLP reducts to a more extensive syntax. Remember Example 2 that used an extension of FLP semantics due to [Truszczy´nski, 2010]. In Example 2, the main reason why model T was considered an intended model was that "a∨not a" was assumed to be supported (something that cannot be assumed in intuitionistic logic for example). Indeed, in stable model semantics, one cannot assume such a thing. For example, consider program Π := {a ← not a}. According to stable model semantics, Π has no stable model and, thus, should not have any supported model either. However, assuming that (a ∨ not a) is supported makes us believe that model S := {a} is supported. So, although classically valid, (a ∨ not a) is not supported.

The last semantics that we discuss in this section is yet another extension of FLP semantics. This extension is called the semantics of well-justified FLP answer sets [Shen and Wang, 2012]. This semantics is different from the extension given in [Truszczy´nski, 2010] even over the class of propositional programs. The motivation behind development of [Shen and Wang, 2012] is very similar to ours but their method to address their concern is completely different.

Shen and You [Shen and You, 2009] noticed that standard FLP semantics suffers from self-justification. They addressed this deficiency using an approach similar to that of default logic (over a limited syntax of logic programs with C-atoms). Their approach was extended to other syntactical fragments in [Shen, 2011; Shen and Wang, 2011]. Recently, their approach was extended to general logic programs [Shen and Wang, 2012] that also covers our intended syntactical fragment (full propositional programs).

Although the motivation behind [Shen and Wang, 2012] closely corresponds to ours (i.e., we both aim to remove circular justifications), the approach that we take towards this goal is completely different. We start from our definition that is given in terms of intuitionistic derivability and is completely declarative (i.e., intended models are characterized in terms of their properties and not operationally). However,

[Shen and Wang, 2012] takes an operational approach and uses an immediate consequence operator (a generalization of van Emden-Kowalski one-step provability operator [van Emden and Kowalski, 1976]) to describe their intended models.

Apart from the methodological difference above, there also exist propositional programs that have different intended models according to our supported semantics relative to welljustified FLP semantics. For example, consider the following program Π3:

Firstly, note that program Π3 above is acceptable in both our syntax and the syntax of general logic programs (as in [Shen and Wang, 2012]). Secondly, note that the second rule "(a ∨ ¬a) ← ⊤", although trivial in classical logic, is not purposeless in programΠ3 above.

Program Π3 in Equation (6) is intuitively read as follows: second rule says that either a or ¬a has to be believed. However, according to the first rule, even if ¬a is believed, a has to be believed too. So, since one of a or ¬a has to be believed and since in both cases a is believed, according to Π3, a must be believed. Thus, model S := {a} is the only intended model of Π3.

Indeed, in supported semantics, {a} is the only supported model of Π3. However, according to the well-justified FLP semantics, Π3 has no well-justified model and here is why:

According to well-justified FLP semantics [Shen and Wang, 2012], fΠS3 = {(a ∨ ¬a) ← ⊤} because the body of the rule "a ← ¬a" is not satisfied by S and thus this rule is removed. Since S = {a}, we have that S- = ∅ and, thus, ¬S- = ∅. Therefore, T α fΠS3 (∅, ¬S-) = T α fΠS3 (∅, ∅) = {(a ∨ ¬a)}1 . Now, according to well-justified FLP semantics, S is accepted if and only if S is a classical consequence of T α fΠS3 (∅, ¬S-)∪¬S-. However, since ¬S- = ∅, we have that T α fΠS3 (∅, ¬S-)∪¬S- = {(a∨¬a)}. Obviously, a ∈ S is not a consequence of "a∨¬a" and, thus, S is not an intended model of Π3 according to well-justified FLP semantics introduced in [Shen and Wang, 2012].

Discussions above show that our semantics is more suited to extend stable models to the full propositional language. A more thorough investigation of how our supported semantics relates to different extensions of FLP semantics is still needed.

5 Complexity

We defined supported semantics and proved some natural connections between supported semantics and other wellestablished semantics including stable models, Kripke models, HT-models, equilibrium models, minimal classical models and Clark completion models. Except for Kripke models, deciding about the validity, satisfiability or falsity of a program in those other semantics are relatively easy (decidable in the second level of polynomial hierarchy in the worst case). However, for Kripke models, deciding whether a propositional program Π is a tautology (i.e., Π is true in all Kripke models) is PSPACE-complete [Ladner, 1977; Svejdar, 2003].

1T α fΠI (∅, ¬I -) is the least fixpoint of an operator that generalizes van Emeden-Kowalski one-step provability operator and is introduced in [Shen and Wang, 2012].

In this section we investigate the computational complexity of (1) checking whether a propositional model S is a supported model of a propositional program Π with respect to a universe U of propositional atoms, and, (2) doing cautious/brave reasoning for a propositional program P. Obviously, in this section, we assume that all three parts P, S and U are finite.

Let us first review what we already know about the computational complexity of finding a supported model (or checking if a given S is supported). On one hand, as disjunctive stable models coincide with supported models over the class of disjunctive logic programs, we know that (1) checking supported-ness of a given S is ΠP1 -hard, (2) brave reasoning about supported models is ΣP2 -hard, and, (3) cautious reasoning about supported models is ΠP2 -hard.

On the other hand, by PSPACE-completeness of checking if a formula is an intuitionistic tautology, we also know that checking if a given S is a supported model can be done in PSPACE. The following theorem closes the gap between our lower bound (second level of PH) and upper bound (PSPACE) by proving that it is ΠP1 -complete to decide if a given S is supported:

Theorem 6 (Complexity of Decision Procedure). Let P be a finite propositional program, U be a finite universe of propositional atoms and S be a subset of U. Then, the problem of deciding whether S is a supported model of P with respect to universe U is a ΠP1 -complete problem.

Using Theorem 6, we can also characterize the complexity of brave/cautious reasoning about supported models:

Corollary 2 (Complexity of Brave/Cautious Reasoning). Let P be a finite propositional program and U be a finite universe of propositional atoms and ST , SF ⊆ U. Then,

1. it is a ΣP2 -complete task to decide if there exists S such that (1) ST ⊆ S, (2) S ∩ SF = ∅, and (3) S is a supported model of P with respect to universe U (brave reasoning).
2. it is a ΠP2 -complete task to decide if all supported models S of P with respect to universe U satisfy both ST ⊆ S and S ∩ SF = ∅ (cautious reasoning).

6 Conclusion and FutureWorks

In this paper, we extended the well-established stable model semantics of logic programs to the full propositional case. Indeed, our extension is not the first try towards this goal. However, the main difference between our approach and previous approaches is that we are not concerned with an arbitrary semantics whose only relation to stable models is that it agrees with stable model semantics over the class of logic programs. Instead, the novelty of our approach is to start with the fundamental ideas that motivated the stable models in the first place. Starting from such fundamentals, equivalence of supported semantics and stable model semantics (over the class of logic programs) is a necessary consequence of our approach rather than a surprising coincidence.

This paper also studied the connection between some of the proposed semantics for non-monotonic reasoning and our supported model semantics. There are still many semantics for non-monotonic reasoning (such as default logic and autoepistemic logic) for which the relation to our supported model semantics is not known. We hope that a detailed study of this relation reveals a deep and intrinsic connection between our semantics and other well-established frameworks for non-monotonic reasoning.

The last topic that we covered in this paper is the complexity of reasoning about supported models. We proved that although we used intuitionistic reasoning to guarantee supportedness of models, none of the interesting reasoning tasks becomes more computationally complex than before (when supportedness was not a concern).

One of the topics that we will deal with in another paper is to develop an efficient mechanism to reason about supported models.