key: cord-0281454-ue0rjd2h
authors: Charalambidis, Angelos; Rondogiannis, Panos; Troumpoukis, Antonis
title: A Logical Characterization of the Preferred Models of Logic Programs with Ordered Disjunction
date: 2021-08-07
journal: nan
DOI: 10.1017/s1471068421000235
sha: 7b93f55540bfe9add6eea62c47fa867e590b8460
doc_id: 281454
cord_uid: ue0rjd2h

Logic Programs with Ordered Disjunction (LPODs) extend classical logic programs with the capability of expressing alternatives with decreasing degrees of preference in the heads of program rules. Despite the fact that the operational meaning of ordered disjunction is clear, there exists an important open issue regarding its semantics. In particular, there does not exist a purely model-theoretic approach for determining the most preferred models of an LPOD. At present, the selection of the most preferred models is performed using a technique that is not based exclusively on the models of the program and in certain cases produces counterintuitive results. We provide a novel, model-theoretic semantics for LPODs, which uses an additional truth value in order to identify the most preferred models of a program. We demonstrate that the proposed approach overcomes the shortcomings of the traditional semantics of LPODs. Moreover, the new approach can be used to define the semantics of a natural class of logic programs that can have both ordered and classical disjunctions in the heads of clauses. This allows programs that can express not only strict levels of preferences but also alternatives that are equally preferred. This work is under consideration for acceptance in TPLP.

Logic Programs with Ordered Disjunction (LPODs) extend classical logic programs with the capability of expressing ordered alternatives in the heads of program rules. In particular, LPODs allow the head of a program rule to be a formula C 1 × · · · × C n , where "×" is a propositional connective called "ordered disjunction" and the C i 's are literals. The intuitive explanation of C 1 × · · · × C n is "I prefer C 1 ; however, if C 1 is impossible, I can accept C 2 ; · · · ; if all of C 1 , . . . , C n−1 are impossible, I can accept C n ". Due to their simplicity and expressiveness, LPODs are a widely accepted formalism for preferential reasoning, both in logic programming and in artificial intelligence.

At present, the semantics of LPODs is defined (Brewka 2002; based on the answer set semantics, using a two-phase procedure. In the first phase, the answer sets of the LPOD are produced. This requires a modification of the standard definition of answer sets. In the second phase, the answer sets are "filtered", and we obtain the set of "most preferred " answer sets, which are taken as the meaning of the initial program. Notice that both phases are not purely model-theoretic: the first one requires the construction of the reduct of the program and the second one is performed using the so-called "degree of satisfaction of rules", a concept that relies on examining the rules of the program to justify the selection of the most preferred answer sets. Apart from its logical status, the current semantics of LPODs produces in certain cases counterintuitive most preferred answer sets. This discussion leads naturally to the question: "Is it possible to specify the semantics of LPODs in a purely model-theoretic way? ".

An important first step in this direction was performed by Cabalar (2011) , who used Equilibrium Logic (Pearce 1996) to logically characterize the answer sets produced in the first phase described above. However, to our knowledge, the second phase (namely the selection of the most preferred answer sets), has never been justified model-theoretically. We consider this as an important shortcoming in the theory of LPODs. Apart from its theoretical interest, this question also carries practical significance, because, as we are going to see, the present formalization of the second phase produces in certain cases counterintuitive (and in our opinion undesirable) results. The main contribution of the present paper is to provide a purely model-theoretic characterization of the semantics of LPODs. The more specific contributions are the following:

• We propose a new semantics for LPODs which uses an additional truth value in order to select as most preferred models those in which a top preference fails only if it is impossible to be satisfied. We demonstrate that the proposed approach overcomes the shortcomings of the traditional semantics of LPODs. In this way, the most preferred models of an LPOD can be characterized by a preferential ordering of its models. • We demonstrate that our approach can be seamlessly extended to programs that allow both ordered and classical disjunctions in the heads of clauses. In particular, we define a natural class of such programs and demonstrate that all our results about LPODs transfer, with minimal modifications, to this new class. In this way we provide a clean semantics for a class of programs that can express not only strict levels of preference but also alternatives that are equally preferred.

Section 2 introduces LPODs and gives relevant background. Sections 3 and 4 describe the shortcomings of LPOD semantics and give an intuitive presentation of the proposed approach for overcoming these issues. The remaining sections give a technical exposition of our results. The proofs of all results have been moved to corresponding appendices.

Logic programs with ordered disjunction are an extension of the logic programs introduced by Gelfond and Lifschitz (1991) , called extended logic programs, which support two types of negation: default (denoted by not) and strong (denoted by ¬). Strong negation is useful in applications but it is not very essential from a semantics point of view: a literal ¬A is semantically treated as an atom A . For the basic notions regarding extended logic programs, we assume some familiarity with the work of Gelfond and Lifschitz (1991) .

Definition 1 A (propositional) LPOD is a set of rules of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k where the C i , A j , and B l are ground literals.

The intuitive explanation of a formula C 1 × · · · × C n is "I prefer C 1 ; however, if C 1 is impossible, I can accept C 2 ; · · · ; if all of C 1 , . . . , C n−1 are impossible, I can accept C n ". An interpretation of an LPOD is a set of literals. An interpretation is called consistent if there does not exist any atom A such that both A and ¬A belong to I. The notion of model of an LPOD is defined as follows.

Let P be an LPOD and M an interpretation. Then, M is a model of P iff for every rule To obtain the preferred answer sets of an LPOD, a two-phase procedure was introduced by Brewka (2002) . In the first phase, the answer sets of the LPOD are produced. This requires a modification of the standard definition of answer sets for extended logic programs. In the second phase, the answer sets are "filtered", and we obtain the set of "most preferred" ones. The first phase is formally defined as follows.

Let P be an LPOD. The ×-reduct of a rule R of P of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k with respect to a set of literals I, is denoted by R I × and is defined as follows:

. . , A m | C i ∈ I and I ∩ {C 1 , . . . , C i−1 , B 1 , . . . , B k } = ∅} The ×-reduct of P with respect to I is denoted by P I × and is the union of the reducts R I × for all R in P .

A set M of literals is an answer set of an LPOD P if M is a consistent model of P and M is the least model of P M × .

The second phase produces the "most preferred" answer sets using the notion of the degree of satisfaction of a rule. Formally:

Let M be an answer set of an LPOD P . Then, M satisfies the rule:

The degree of a rule R in the answer set M is denoted by deg M (R).

The satisfaction degrees of rules are then used to define a preference relation on the answer sets of a program. Given a set of literals M , let M i (P ) = {R ∈ P | deg M (R) = i}. The preference relation is defined as follows.

Let M 1 , M 2 be answer sets of an LPOD P . Then, M 1 is inclusion-preferred to M 2 iff there exists k ≥ 1 such that M k 2 (P ) ⊂ M k 1 (P ), and for all j < k, M j 2 (P ) = M j 1 (P ).

Consider the program:

wine × beer. The above program has the answer sets {wine} and {beer}. The most preferred one is {wine} because it satisfies the unique fact of the program with degree 1 (while the answer set {beer} satisfies the fact with degree 2). Consider now the program:

This has the unique answer set {beer} (the set {wine,¬wine} is rejected due to its inconsistency). Therefore, {beer} is also the most preferred answer set.

Notice that Brewka (2002) originally defined only the preference relation of Definition 6. In the follow-up paper ) two more preference relations were introduced, namely the cardinality and the Pareto, in order to treat cases for which the inclusion preference did not return the expected results. All these relations do not rely exclusively on the models of the source program, and are therefore subject to similar criticism. For this reason, in this paper we focus attention on the inclusion preference relation.

From a foundational point of view, the main issue with the semantics of LPODs is that, in its present form, it is not purely model-theoretic. Despite the simplicity and expressiveness of ordered disjunction, one can not characterize the meaning of a program by just looking at its set of models. Recall that this principle is one of the cornerstones of logic programming since its inception: the meaning of positive logic programs is captured by their minimum Herbrand model (van Emden and Kowalski 1976) and the meaning of extended logic programs is captured by their equilibrium models (Pearce 1996) . How can the most preferred models of LPODs be captured model-theoretically? The existing issues regarding the semantics of LPODs are illustrated by the following examples.

Consider the following two programs:

According to Definition 2, both programs have exactly the same models, namely {a}, {b}, and {a,b}. Moreover, both have the same answer sets, namely {a} and {b}. However, there is no model-theoretic explanation (namely one based on just the sets of models of the programs) of why the most preferred model of the first program is {a} while the most preferred model of the second program is {b}. As a conclusion, in order for the semantics of LPODs to be properly specified, a model-based approach needs to be devised.

Apart from the fact that Definition 5 is not purely model-theoretic, in many cases it also gives inaccurate preferential orderings of answer sets. Such inaccurate orderings have already been reported in the literature (Balduccini and Mellarkod 2003) . The following program illustrates one such simple case.

Consider the following program 1 whose declarative reading is "I prefer to buy a Mercedes than a BMW. In case a Mercedes is available, I prefer a gas model to a diesel one. A gas model (of Mercedes) is not available". mercedes × bmw. gas mercedes × diesel mercedes ← mercedes. ¬gas mercedes.

The program has two answers sets: M 1 = {mercedes, diesel mercedes, ¬gas mercedes} and M 2 = {bmw, ¬gas mercedes}. M 1 satisfies the first rule with degree 1, the second rule with degree 2, and the third rule with degree 1. M 2 satisfies the first rule with degree 2, the second rule with degree 1 (because the body of the rule evaluates to false), and the third rule with degree 1. According to Definition 6, the two answer sets are incomparable. However, it seems reasonable that the most preferred model is M 1 : the first rule, which is a fact, specifies unconditionally a preference; the preferences of the second rule seem to be secondary, because they depend on the choice that will be made in the first rule.

The problems in the above example appear to be related to Definition 5: it assigns degree 1 in two cases that are apparently different: a rule that has a false body gets the same degree of satisfaction as a rule with a true body in whose head the first choice is satisfied. These are two different cases which, however, it is not obvious how to handle if we follow the satisfaction degree approach of Definition 5.

It has been remarked , discussion in page 342) that the inclusionpreference is sensitive to the existence of unsatisfiable better options. The following example, taken from the paper by , motivates this problem.

Assume we want to book accommodation for a conference (in the post-COVID era). We prefer a 3-star hotel from a 2-star hotel. Moreover, we prefer to be in walking distance from the conference venue. This can be modeled by the program:

walking × ¬walking.

Consider now the scenario where the only available 3-star hotel (say hotel 1 ), is not in walking distance. Moreover, assume that the only available 2-star hotel (say hotel 2 ), happens to be in walking distance. According to Definition 6, these two options are incomparable because hotel 1 satisfies the first rule to degree 2 and the second rule to degree 1, while hotel 2 satisfies the first rule to degree 1 and the second rule to degree 2.

Assume now that the above program is revised after learning that there also exists a 4-star hotel, which however is not an option for us (due to restrictions imposed by our funding agencies). The new program is:

In the new program, hotel 1 satisfies the first rule to degree 2 and the second rule to degree 2, while hotel 2 satisfies the first rule to degree 1 and the second rule to degree 3. According to Definition 6, hotel 2 is our preferred option.

The above example illustrates that under the "degree of satisfaction of rules" semantics, a small (and seemingly innocent) change in the program, can cause a radical change in the final preferred model. This sensitivity to changes is another undesirable consequence that stems from the fact that the second phase of the semantics of LPODs is not purely model-theoretic.

The main purpose of this paper is to define a model-theoretic semantics for LPODs. In other words, we would like to be able to choose the most preferred answer sets of a program using preferential reasoning on the answer sets themselves. Actually, such an approach should also be applicable directly on the models of the source program, without the need to first construct the answer sets of the program. We would expect that such an approach would also provide solutions to the shortcomings of the previous section.

But on what grounds can we compare the answer sets (or, even better, the models) of a program and decide that some of them satisfy in a better way our preferences than the others? This seems like an impossible task because the answer sets (or the models) do not contain any information related to the ordered disjunction preferences of the program.

It turns out that we can introduce preferential information inside the answer sets of a program by slightly tweaking the underlying logic. The answer sets of extended logic programs are two-valued, ie., a literal is either T (true) or F (false). We argue that in order to properly define the semantics of LPODs, we need a third truth value, which we denote by F * . The intuitive reading of F * is "impossible to make true".

To understand the need for F * , consider again the intuitive meaning of C 1 × C 2 : we prefer C 2 only if it is impossible for us to get C 1 . Impossible here means that if we try to make C 1 true, then the interpretation will become inconsistent. Therefore, we seem to need two types of false, namely F and F * : F means "false by default" while F * means "impossible to make true". The following example demonstrates these issues.

Consider the program:

wine × beer. ¬wine.

As we are going to see in the coming sections, the most preferred answer set according to our approach is {(wine, F * ), (beer, T ), (¬wine, T )}. Notice that wine receives the value F * because if we tried to make wine equal to T , the interpretation would become inconsistent (because ¬wine is T ). Notice also that, as we are going to see, the interpretation {(wine, F ), (beer, T ), (¬wine, T )} is not a model of the program.

The above discussion suggests the following semantics for "×" in the proposed logic.

Let u, v ∈ {F, F * , T }. Then:

The intuition of the above definition is that we return the value v only if it is impossible to satisfy u; in all other cases, we return u.

We now get to the issue of how we can use the value F * to distinguish the most preferred answer sets: we simply identify those answer sets that are minimal with respect to their sets of atoms that have the value F * . As we have mentioned, the value F * means "impossible to make true". By minimizing with respect to the F * values, we only keep those answer sets in which a top preference fails only if it is impossible to be satisfied.

The above discussion gives a description of how we can select the "most preferred (three-valued) answer sets" of an LPOD. However, it is natural to wonder whether it is possible to also characterize the answer sets model-theoretically, completely circumventing the construction of the reduct. A similar question was considered by Cabalar (2011) , who demonstrated that the (two-valued) answer sets of an LPOD coincide with the equilibrium models of the program. We adapt Cabalar's characterization to fit in our setting. More specifically, we extend our three-valued logic to a four-valued one by adding a new truth value T * , whose intuitive meaning is "not false but its truth can not be established ". We then demonstrate that the three-valued answer sets of an LPOD P are those models of P that are minimal with respect to a simple ordering relation and do not contain any T * values. In this way we get a two-step, purely model-theoretic characterization of the most-preferred models of LPODs: in the first step we use the T * values as a yardstick to identify those models that correspond to answer-sets, and in the second step we select the most preferred ones, by minimizing with respect to the F * values.

Finally, we consider the problem of characterizing the semantics of logic programs that contain both disjunctions and ordered disjunctions in the heads of rules. This is especially useful in cases where some of our preferences are equally important. For example:

(wine ∨ beer) × (soda ∨ juice).

states that wine and beer are our top preferences (but we have no preference among them), and soda and juice are our secondary preferences. We consider the class of programs in which the heads of rules consist of ordered disjunctions where each ordered disjunct is an ordinary disjunction (as in the above program). We demonstrate that the theory of these programs is very similar to that of LPODs. All our results for LPODs transfer with minimal modifications to this extended class of programs. This suggests that this is a natural class of programs that possibly deserves further investigation both in theory and in practice.

In this section we provide a new definition of the answer sets of LPODs. The new definition is based on a three-valued logic which allows us to discriminate the most preferred answer sets using a purely model-theoretic approach. In Section 6 we demonstrate that by extending the logic to a four-valued one, we can identify directly the most preferred models of a program (without first producing the answer sets).

Let Σ be a nonempty set of propositional literals. The set of well-formed formulas is inductively defined as follows:

• Every element of Σ is a well-formed formula, • The 0-place connective F * is a well-formed formula, • If φ 1 and φ 2 are well-formed formulas, then (φ 1 ∧ φ 2 ), (φ 1 ∨ φ 2 ), (not φ 1 ), (φ 1 ← φ 2 ), and (φ 1 × φ 2 ), are well-formed formulas.

The meaning of formulas is defined over the set of truth values {F, F * , T } which are ordered as

Definition 8 A (three-valued) interpretation I is a function from Σ to the set {F, F * , T }. We can extend I to apply to formulas, as follows:

It is straightforward to see that the meanings of "∨", "∧", and "×" are associative and therefore we can write I(φ 1 ∨· · ·∨φ n ), I(φ 1 ∧· · ·∧φ n ), and I(φ 1 ×· · ·×φ n ) unambiguously (without the need of extra parentheses). Moreover, given literals C 1 , . . . , C n we will often write I(C 1 , . . . , C n ) instead of I(C 1 ∧ · · · ∧ C n ).

The ordering < (respectively, ≤) on truth values extends in the standard way on interpretations: given interpretations I 1 , I 2 we write I 1 < I 2 (respectively, I 1 ≤ I 2 ), if for all literals L ∈ Σ, I 1 (L) < I 2 (L) (respectively, I 1 (L) ≤ I 2 (L)).

When we consider interpretations of an LPOD program, we assume that the underlying set Σ is the set of literals of the program. The following definition will be needed.

An interpretation I is a model of an LPOD P if every rule of P evaluates to T under I. An interpretation I of P is called consistent if there do not exist literals A and ¬A in P such that I(A) = I(¬A) = T .

We can now give the new definitions for reduct and answer sets for LPODs.

Let P be an LPOD. The ×-reduct of a rule R of P of the form:

with respect to an interpretation I, is denoted by R I × and is defined as follows:

× is the set that contains the rules:

where r is the least index such that I(C 1 ) = · · · = I(C r−1 ) = F * and either r = n or I(C r ) = F * .

The ×-reduct of P with respect to I is denoted by P I × and is the union of the reducts R I × for all R in P .

The major difference of the above definition from that of Definition 3, are the clauses of the form C i ← F * , A 1 , . . . , A m . These clauses are included so as that the value F * can be produced for C i when I(A 1 ) = · · · = I(A m ) = T . Notice that if these clauses did not exist, there would be no way for the value F * to be produced by the reduct.

Let P be an LPOD and M an interpretation of P . We say that M is a (three-valued)

Notice that the least model of P M × in the above definition, can be constructed using the following immediate consequence operator

Notice that since the set {F, F * , T } is a complete lattice under the ordering ≤, it is easy to see that the set of interpretations is also a complete lattice under the ordering ≤. Moreover, the operator T P M × is monotonic over the complete lattice of interpretations; this follows from the fact that the meanings of conjunction (namely, min) and that of disjunction (namely, max), are monotonic. Then, by Tarski's fixed-point theorem, T P M × has a least fixed-point, which can be easily shown to be the ≤-least model of P M × . The following lemma guarantees that our definition is a generalization of the well-known one for extended logic programs (Gelfond and Lifschitz 1991) .

Let P be a consistent extended logic program. Then the three-valued answer sets of P coincide with the standard answer sets of P .

The following lemmas, which hold for extended logic programs, also extend to LPODs.

Let P be an LPOD and let M be an answer set of P . Then, M is a model of P .

Let M be a model of an LPOD P . Then, M is a model of P M × .

The answer sets of extended logic programs are minimal with respect to the classical truth ordering F < T . As it turns out, the answer sets of LPODs are minimal but with respect to an extended ordering, which is defined below.

The ordering ≺ on truth values is defined as follows:

Given interpretations I 1 , I 2 , we write I 1 ≺ I 2 (respectively, I 1 I 2 ) if for all literals L ∈ Σ * , I 1 (L) ≺ I 2 (L) (respectively, I 1 (L) I 2 (L)).

Every (three-valued) answer set M of an LPOD P , is a -minimal model of P .

As in the case of the original semantics of LPODs, we now need to define a preference relation over the answer sets of a program. Intuitively, we prefer those answer sets that maximize the prospect of satisfying our top choices in ordered disjunctions. This can be achieved by minimizing with respect to F * values. More formally, we define the following ordering:

Let P be an LPOD and let M 1 , M 2 be answer sets of P . Let M * 1 and M * 2 be the sets of literals in M 1 and M 2 respectively that have the value F * . We say that M 1 is preferred

Definition 14 An answer set of an LPOD P is called most preferred if it is minimal among all the answer sets of P with respect to the relation.

The intuition behind the definition of is that we prefer those answer sets that minimize the need for F * values. In other words, an answer set will be most preferred if all the literals that get the value F * , do this because there is no other option: these literals must be false in order for the program to have a model. We now examine the examples of Section 3 under the new semantics introduced in this section.

Consider again the two programs discussed in Subsection 3.1. Under the proposed approach, the first program has two answer sets, namely {(a, T ), (b, F )} and {(a, F * ), (b, T )}, and the most preferred one (ie., the minimal with respect to ) is {(a, T ), (b, F )}. The second program also has two answer sets, namely {(a, F ), (b, T )} and {(a, T ), (b, F * )}, and the most preferred one is {(a, F ), (b, T )}. Notice that now the two programs have different sets of models and different answer sets and therefore it is reasonable that they have different most preferred ones.

Consider the "cars" program of Subsection 3.2. It is easy to see that it has two answer sets, namely:

According to the ordering, the most preferred answer set is M 1 .

Consider the "hotels" program from Subsection 3.3. Under the restriction that there does not exist any 3-star hotel in walking distance and also there does not exist any 2-star hotel outside walking distance, we get the two incomparable answer sets:

Consider now the modified program given in Subsection 3.3 (which contains the unsatisfiable better option of a 4-star hotel). Under the same restrictions as above, we get the two answer sets:

Under the proposed approach, the above two answer sets are also incomparable, and the problem identified in Subsection 3.3 no longer exists.

We close this section by stating a result that establishes a relationship between the answer sets produced by our approach (Definition 4) and those ones produced by the original formulation (Brewka 2002; ).

Let I be a three-valued interpretation of LPOD P . We define collapse(I) to be the set of literals L in P such that I(L) = T .

Let P be an LPOD and M be a three-valued answer set of P . Then, collapse(M ) is an answer set of P according to Definition 4.

Let N be an answer set of P according to Definition 4. There exists a unique three-valued interpretation M such that N = collapse(M ) and M is a three-valued answer set of P .

In other words, there is a bijection between the answer sets produced by our approach and the original ones. Moreover, each three-valued answer set only differs from the corresponding two-valued one in that some literals of the former may have a F * value instead of an F value. However, these F * values play an important role because they allow us to distinguish the most preferred answer sets.

In this section we demonstrate that the answer sets of LPODs can be characterized in a purely logical way, namely without even the use of the reduct. In particular, we demonstrate that the answer sets of a given program P coincide with a well-defined subclass of the minimal models of P in a four-valued logic. This logic is an extension of the three-valued one introduced in Section 5 and minimality is defined with respect to a four-valued relation that extends the three-valued one of Definition 12. The new logic is based on four truth values, ordered as follows:

The value T * can be read as "not false but its truth can not be established ". The connections of this logic with Equilibrium Logic (Pearce 1996) are discussed in Section 8. An interpretation is now a function from Σ to the set {F, F * , T * , T }. The semantics of formulas with respect to an interpretation I is defined identically as in Definition 8. The notions of interpretation, consistent interpretation, and model are defined as in Definition 9. Moreover, we extend the three-valued relation of Definition 12, as follows: 

The (four-valued) ordering ≺ is defined as follows:

Given interpretations I 1 , I 2 of a program P , we write I 1 ≺ I 2 (respectively, I 1 I 2 ) if for all literals L in P , I 1 (L) ≺ I 2 (L) (respectively, I 1 (L) I 2 (L)).

The following special kind of interpretations plays an important role in our logical characterization.

We can now state the logical characterization of the answer sets of an LPOD.

Let P be an LPOD. Then, M is a three-valued answer set of P iff M is a consistent -minimal model of P and M is solid.

In conclusion, given an LPOD we can purely logically characterize its most preferred models by first taking its consistent -minimal models that are solid and then keeping the -minimal ones (see Definitions 13 and 14).

An extended study of the properties of the proposed four-valued logic is outside the scope of the present paper. Figure 1 lists some useful equivalences; the first column is for classical connectives, while the second column contains equivalences involving the "×" operator. We note the interaction of × with ∨ because this will be the central theme of the next section. It is easy to see that:

We note that this equivalence does not hold, a fact which will be referenced in the next section.

We now extend the ideas of the previous sections to programs that also allow standard disjunctions in the heads of rules. The case of disjunctive LPODs (DLPODs), was initially considered by Kärger et al. (2008) and reexamined by Cabalar (2011) .

The main idea of using disjunctions in the heads of LPOD rules is described (Kärger et al. 2008) as follows: "we use ordered disjunction to express preferences and disjunction to express indifferences".

Example 8 (taken from the paper by Kärger et al. (2008) ) The program:

expresses the fact that our top choice is going to the pub; if this is not possible, then our secondary preference can be satisfied by either going to the cinema or watching tv. Kärger et al. (2008) consider rules whose heads are arbitrary combinations of atoms and the operators × and ∨. A set of transformations is then used in order to bring the heads of rules into "Ordered Disjunctive Normal Form (ODNF)". More specifically, each head is transformed into a formula of the form C 1 ∨ · · · ∨ C n where each C i is an ordered disjunction of literals. The resulting normalized rules are then used to obtain the preferred answer sets of the original program.

The program of Example 8 is transformed to:

This program is then used to get the preferred answer sets of the original one.

However, as observed by Cabalar (2011) , one of the transformations used by Kärger et al. (2008) to obtain the ODNF, can not be logically justified: the formula (φ 1 ∨ φ 2 ) × φ 3 is not logically equivalent to the formula (φ 1 × φ 3 ) ∨ (φ 2 × φ 3 ) in terms of the logic of Here-and-There. As discussed at the end of Section 6, these two formulas are also not equivalent under our four-valued logic.

As an alternative approach to the semantics of DLPODs, Cabalar (2011) proposes to use the logical characterization on rules with heads that are arbitrary combinations of disjunctions and ordered disjunctions. We could extend this approach to get a logical characterization of the most preferred models of arbitrary DLPODs: given such a program P , we could at first consider all the -minimal models of P that are solid, and then select the -minimal among them. Such an approach is certainly general. However, we believe that not every such program carries computational intuition. A good example of this is given in (Cabalar 2011, Example 2) , where a program with both disjunction and ordered disjunction is given, and whose computational meaning is far from clear.

In the following, we define a class of programs which, as we claim, have a clear computational interpretation and at the same time retain all properties that we have identified for LPODs. Intuitively, we allow the head of a program rule to be a formula C 1 × · · · × C n where each C i is an ordinary disjunction of literals. Notice that the program in Example 8 belongs to this class, while the program in Example 9, does not. We believe that the programs of this class have a clear preferential interpretation. Intuitively, the rule heads of the programs we consider, denote a hierarchy of preferences imposed by the × operator; in each level of this hierarchy, we may have literals that have equal preference (this is expressed by standard disjunction).

It is important to stress that if we allowed arbitrary combinations of disjunctions and ordered disjunctions, the preferential intuition would be lost. To see this, consider for example the formula (a × b) ∨ (c × d). This gives us the information that (a × b) is at the same level of preference as (c × d), and that a is more preferred than b and c is more preferred than d; however, for example, it gives us no information of whether a is more preferred than c. On the other hand, a formula of the fragment we consider, such as (a ∨ b) × (c ∨ d) gives us a total order of a, b, c, and d.

A (propositional) DLPOD is a set of rules of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k where the A j and B l are ground literals and each C i is a disjunction of ground literals.

As it turns out, the answer sets of such programs can be defined in an almost identical way as those of LPODs.

Let P be a DLPOD. The ×-reduct of a rule R of P of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k with respect to an interpretation I, is denoted by R I × and is defined as follows:

× is the set that contains the rules:

where r is the least index such that I(C 1 ) = · · · = I(C r−1 ) = F * and either r = n or I(C r ) = F * .

The ×-reduct of P with respect to I is denoted by P I × and is the union of the reducts R I × for all R in P .

Let P be a DLPOD and M a (three-valued) interpretation of P . Then, M is an answer set of P if M is consistent and M is a minimal model of the disjunctive program P M × . As it turns out, all the results we have obtained in the previous section, hold for DLPODs. The proofs of these results are (surprisingly) almost identical (modulo some minor notational differences) to the proofs of the corresponding results for LPODs. For reasons of completeness, the corresponding proofs are given in the appendix. The extended results are stated below.

Let P be a consistent disjunctive extended logic program. Then, the answer sets of P according to Definition 20, coincide with the standard answer sets of P .

Let P be a DLPOD and let M be an answer set of P . Then, M is a model of P .

Let M be a model of a DLPOD P . Then, M is a model of P M × .

Lemma 10 Every answer set M of a DLPOD P , is a -minimal model of P .

Let P be a DLPOD. Then, M is an answer set of P iff M is a consistent -minimal model of P and M is solid.

The similarity of the definitions and of the theoretical results of DLPODs to those of standard LPODs, makes us believe that this is indeed an interesting class of programs that deserves further attention.

The work on LPODs is closely related to "Qualitative Choice Logic" (QCL) . QCL is an extension of propositional logic with the preferential connective "×", which has the same intuitive meaning as in LPODs: A×B is read "if possible A, but if A is impossible then at least B". Essentially, QCL is the propositional logic underlying LPODs. It is worth noting that the semantics of QCL is based on the "degree of satisfaction" of formulas, which is connected to the idea of the degree of satisfaction of the rules of LPODs (Definition 5). Moreover, as remarked by one of the reviewers of the present paper, the DLPODs introduced in Section 7 are closely connected to the "basic choice formulas" of QCL , Section 3.1, Definition 8). It would be interesting to investigate whether our four-valued logic can be used to provide an alternative semantics for QCL.

The work reported in this paper is closely connected to the work of Cabalar (2011), who first considered the problem of expressing logically the semantics of LPODs. The key difference between the two works is that ours provides a characterization of both phases of the production of the most preferred models of an LPOD, while Cabalar's work concentrates on the first one.

It is important to stress here that both our work as well as the work of Cabalar (2011), are influenced by the work of Pearce (1996) who first gave a logical characterization of the answer sets of extended logic programs, using Equilibrium Logic. This is a non-monotonic logic which is defined on top of the monotonic logic of Here-and-There (Heyting 1930 ), using a model preference approach. The technique we have proposed in this paper, when applied to a consistent extended logic program P , produces the standard answer sets of P ; this is a direct consequence of Theorem 1 and Lemma 1. Therefore, for extended logic programs, the Equilibrium Logic gives the same outcome as our approach which is based on a four-valued logic and -minimal models that are solid. We believe that a further investigation of the connections of our approach with that of Equilibrium Logic is a worthwhile topic.

Our work is the first to provide a purely model-theoretic characterization of the semantics of LPODs. To our knowledge, the four-valued logic we have utilized does not appear to be a well-known variant/extension of Here-and-There. However, some seemingly related logics have been used in the literature of answer set extensions. The original definition of Equilibrium Logic included a second constructive negation, which corresponds to Nelson's strong negation (Nelson 1949) . This gave rise to a five-valued extension of Here-and-There, called N 5 . Also, a logic called X 5 , that is closely connected to N 5 , was recently proposed by Aguado et al. (2019) in order to capture the semantics of arbitrary combinations of explicit negation with nested expressions. Both N 5 and X 5 appear to be connected to our four-valued logic due to the different notions of false and true that they employ in order to capture aspects that arise in answer set semantics. However, the ordering of the truth values and the semantics of the logical connectives are different, and the exact correspondence (if any) between these logics and the present one, is not straightforward to establish. This is certainly an interesting topic for further investigation.

Another promising topic for future work is the characterization of the notion of strong equivalence (Lifschitz et al. 2001) for LPODs and DLPODs. When two logic programs are strongly equivalent, we can replace one for the other inside a bigger program without worrying that the semantics of the bigger program will be affected. Characterizations of strong equivalence for LPODs have already been obtained by Faber et al. (2008) . It would be interesting to investigate if the logical characterization of the semantics of LPODs and DLPODs developed in the present paper, can offer advantages compared with their work.

Lemma 1 Let P be a consistent extended logic program. Then the three-valued answer sets of P coincide with the standard answer sets of P .

By taking n = 1 in Definition 10, we get the standard definition of reduct for consistent extended logic programs.

Let P be an LPOD and let M be an answer set of P . Then, M is a model of P .

Consider any rule R in P of the form:

But then, the body of the rule R evaluates to F under M , and therefore M satisfies R. Consider now the case where R M × is nonempty and consists of the following rules: Case 2: M (A 1 , . . . , A m ) = F * . This implies that M (C r ) ≥ F * . We distinguish two subcases. If r = n then M (C 1 × · · · × C n ) = M (C 1 × · · · × C r ) ≥ F * because, by the definition of P M × it is M (C 1 ) = · · · = M (C r−1 ) = F * and we also know that M (C r ) ≥ F * . Thus, in this subcase M satisfies R. If r < n, then by the definition of P M × , M (C r ) = F * ; however, we know that M (C r ) ≥ F * , and thus M (C r ) = T . Thus, in this subcase M also satisfies R. 

Let M be a model of an LPOD P . Then, M is a model of P M × .

Consider any rule R in P of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k and assume M satisfies R. If M (B i ) = T for some i, 1 ≤ i ≤ k, then no rule is created in P M × for R. Assume therefore that M (not B 1 , . . . , not B k ) = T . By the definition of P M × the following rules have been added to P M × :

where r is the least index such that M (C 1 ) = · · · = M (C r−1 ) = F * and either r = n or M (C r ) = F * . Obviously, the first r − 1 rules above are satisfied by M . For the rule C r ← A 1 , . . . , A m we distinguish two cases based on the value of M (A 1 , . . . , A m ). If M (A 1 , . . . , A m ) = F , then, the rule is trivially satisfied. If M (A 1 , . . . , A m ) > F , then, since rule R is satisfied by M and M (C r ) = F * , it has to be M (C r ) = T . Therefore, the rule C r ← A 1 , . . . , A m is satisfied by M .

Every (three-valued) answer set M of an LPOD P , is a -minimal model of P .

Assume there exists a model N of P with N M . We will show that N is also a model of P M × . Since N M , we also have N ≤ M . Since M is the ≤-least model of P M × , we will conclude that N = M .

Consider any rule R in P of the form:

Assume that R M × is nonempty. This means that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and either r = n or M (C r ) = F * . Then, R M × consists of the following rules:

C 1 ← F * , A 1 , . . . , A m · · · C r−1 ← F * , A 1 , . . . , A m C r ← A 1 , . . . , A m We show that N satisfies the above rules. We distinguish cases based on the value of M (A 1 , . . . , A m ):

Case 1: M (A 1 , . . . , A m ) = F . Then, N (A 1 , . . . , A m ) = F and the above rules are trivially satisfied by N . If  N (A 1 , . . . , A m ) = F then N trivially satisfies all the above rules. Assume therefore that N (A 1 , . . . , A m ) = F * . Recall now that M (C i ) = F * for all i, 1 ≤ i ≤ r − 1. Moreover, it has to be M (C r ) ≥ F * , because otherwise M would not satisfy the rule R. Since N M , it can only be N (C i ) = F * for all i, 1 ≤ i ≤ r − 1 and N (C r ) ≥ F * , because otherwise N would not be a model of P . Therefore, N satisfies the given rules of P M × . If N (A 1 , . . . , A m ) = F then N trivially satisfies all the above rules. Assume therefore that N (A 1 , . . . , A m ) = T . Recall now that M (C i ) = F * for all i, 1 ≤ i ≤ r − 1. Moreover, it has to be M (C r ) = T , because otherwise M would not satisfy the rule R. Since N M , it can only be N (C i ) = F * for all i, 1 ≤ i ≤ r − 1 and N (C r ) = T , because otherwise N would not be a model of P . Therefore, N satisfies the given rules of P M × .

In the proofs that follow, we will use the term Brewka-model to refer to that of Definition 2 and Brewka-reduct to refer to that of Definition 3 (although, to be precise, this definition of reduct was initially introduced in the paper by ).

In order to establish Lemmas 5 and 6 we first show the following three propositions.

Let P be an LPOD and let M be a three-valued model of P . Then, N = collapse(M ) is a Brewka-model of P .

Consider any rule R of P of the form

If there exists A i ∈ N or there exists B j ∈ N then then N trivially satisfies R. Assume that {A 1 , . . . , A m } ⊆ N and {B 1 , . . . , B k } ∩ N = ∅. By Definition 15 it follows that M (A 1 , . . . , A m , not B 1 , . . . , not B k ) = T . Since M is a three-valued model of P , it must satisfy R and therefore M (C 1 × · · · × C n ) = T . Then, there exists r ≤ n such that M (C r ) = T and by Definition 15 we get that C r ∈ N . Therefore, N satisfies rule R.

Let P be an LPOD and M be a Brewka-model of P . Then, M is also a model of the Brewka-reduct P M × .

Consider any rule R in P of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k and assume M satisfies R. If there exists B i ∈ M for some 1 ≤ i ≤ k, then no rule is created in the Brewka-reduct for R. Moreover, if for all i ≤ n, C i ∈ M then also no rule is created in the Brewka-reduct. Assume therefore that {B 1 , . . . , B k } ∩ M = ∅ and there exists r ≤ n such that C r ∈ M and {C 1 , . . . , C r−1 } ∩ M = ∅. By the definition of P M × the only rule added to P M × because of R is C r ← A 1 , . . . , A m . Since C r ∈ M the rule is satisfied by M .

Let P be an LPOD and let M 1 , M 2 be three-valued answer sets of P such that collapse(M 1 ) = collapse(M 2 ). Then, M 1 = M 2 .

Assume, for the sake of contradiction, that M 1 = M 2 . We define:

It is M ≺ M 1 and M ≺ M 2 . We claim that M is a model of P . This will lead to contradiction because, by Lemma 4, M 1 and M 2 are -minimal models of P . Consider any rule R in P of the form: Since, by Lemma 2, M 1 and M 2 are models of P it follows that M 1 (C 1 × · · · × C n ) ≥ F * and M 2 (C 1 × · · · × C n ) ≥ F * . First assume that M 1 (C 1 × · · · × C n ) = T . This implies that there exists 1 ≤ r ≤ n such that M 1 (C r ) = T and M 1 (C i ) = F * for all 1 ≤ i < r.

Since, by assumption collapse(M 1 ) = collapse(M 2 ) it follows that M 2 (C r ) = T and therefore M (C r ) = T . Moreover, it must be M 2 (C i ) = F * for all i < r because we have already established that M 2 (C 1 × · · · × C n ) ≥ F * . Therefore, M (C i ) = F * and M (C 1 × · · · × C n ) = T and M satisfies the rule. Now assume that M 1 (C 1 × · · · × C n ) = F * . It is easy to see that the only case is M 1 (C i ) = F * for all 1 ≤ i ≤ n. Since M 2 has the same collapse with M 1 it follows that M 2 (C i ) ≤ F * and because M 2 (C 1 × · · · × C n ) ≥ F * it also follows that M 2 (C i ) = F * . By definition of M , M (C i ) = F * for all 1 ≤ i ≤ n and M (C 1 × · · · × C n ) = F * . . . , A m ) = T and therefore M 1 (C 1 × · · · × C n ) = T and M 2 (C 1 × · · · × C n ) = T . This implies that there exists r such that M 1 (C 1 ) = M 2 (C 1 ) = F * , . . . , M 1 (C r−1 ) = M 2 (C r−1 ) = F * , and M 1 (C r ) = M 2 (C r ) = T . Therefore, M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) = T , which implies that M (C 1 × · · · × C n ) = T , and therefore M satisfies R.

Let P be an LPOD and M be a three-valued answer set of P . Then, collapse(M ) is an answer set of P according to Definition 4.

Since M is an answer set of P , then by Lemma 2, M is also a model of P . Moreover, by Proposition 1, N = collapse(M ) is a Brewka-model of P . It also follows from Proposition 2 that N is a model of the Brewka-reduct P N . It suffices to show that N is also the minimum model of P N . Assume there exists N that is a model of P N and N ⊂ N . We define M as

It is easy to see that M < M . We will show that M is also model of P M × leading to contradiction because we assume that M is the minimum model of P M × . Consider first a rule of the form C i ← F * , A 1 , . . . , A m . Since M is an answer set of P it must be M (C i ) = F * . By the definition of M it follows that M (C i ) ≥ F * and M satisfies the rule. Now consider a rule of the form C r ← A 1 , . . . , A m . We distinguish cases based on the value of M (A 1 , . . . , A m ). × the rule C r ← A 1 , . . . , A m is a result of a rule in P of the form C 1 × · · · × C r × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k and it must be M (C i ) = F * for all i ≤ r − 1 and M (B j ) ≤ F * for all 1 ≤ j ≤ k. It follows that {C 1 , . . . , C r−1 } ∩ N = ∅ and {B 1 , . . . , B k } ∩ N = ∅. Moreover, since M is a model of P M × we get that M (C r ) = T and it follows that C r ∈ N . By the construction of the Brewka-reduct, there exists a rule C r ← A 1 , . . . , A m in P N . We distinguish two cases. If {A 1 , . . . , A m } ⊆ N then C r ∈ N because N is a model of P N . It follows by the construction of M that M (C r ) = M (C r ) = T and M satisfies the rule. Otherwise, there exists l, 1 ≤ l ≤ m such that A l ∈ N . Notice also that {A 1 , . . . , A m } ⊆ N , so A l ∈ N . Therefore, M (A l ) = F * and M (A 1 , . . . , A m ) ≤ F * . Moreover, since C r ∈ N , we have M (C r ) ≥ F * that satisfies the rule.

Let N be an answer set of P according to Definition 4. There exists a unique three-valued interpretation M such that N = collapse(M ) and M is a three-valued answer set of P .

We construct iteratively a set of literals that must have the value F * in M . Let F n be the sequence:

First we prove that M is a model of P M × . Consider first any rule of the form C i ← F * , A 1 , . . . , A m . By the construction of P M × , such a rule exists because M (C i ) = F * ; therefore M satisfies this rule. Now consider any rule of the form C r ← A 1 , . . . , A m . Such a rule was produced by a rule R in P of the form C 1 × · · · × C r × · · · × C n ← A 1 , . . . , A n , . . . , not B 1 , . . . , not B k .

By the construction of P M × it follows that M (C i ) = F * for all i < r. Therefore C i ∈ N and also C i ∈ F ω for all i < r. Moreover, it must be M (B j ) ≤ F * for all 1 ≤ j ≤ k, so {B 1 , . . . , B k } ∩ N = ∅. We distinguish cases based on the value of M (A 1 , . . . , A m ).

Case 1: If M (A 1 , . . . , A m ) = F then the rule is trivially satisfied by M .

Case 2: If M (A 1 , . . . , A m ) = F * then for some A i , M (A i ) = F * . By the construction of M , it follows that A i ∈ F ω . It follows by the definition of F ω that C r ∈ F ω and therefore M (C r ) ≥ F * .

Case 3: If M (A 1 , . . . , A m ) = T then {A 1 , . . . , A m } ⊆ N and since N is an answer set according to Definition 4 it follows that N is a model of P . It follows that there exists a least j ≤ n such that C j ∈ N . Since we have already established that for all i < r, C i ∈ N it must be r ≤ j ≤ n. But, if r < j then C r ∈ N and by the construction of M it must be M (C r ) = F * . If M (C r ) = F * , then, by the construction of P M × , the rule for C r should be of the form C r ← F * , A 1 , . . . , A m . So, it must j = r and C r ∈ N . Therefore, M (C r ) = T and M satisfies the rule. Therefore, we have established that M is a model of P M × . It remains to show that M is the ≤-least model of P M × . Assume now that there exists M that is a model of P M × and M < M . Let N = collapse(M ). We distinguish two cases.

Case 1: N = N and thus M differs from M only on some atoms C r such that M (C r ) = F and M (C r ) = F * . First, by the construction of M , if M (C r ) = F * then C r ∈ F ω . We show by induction on n that for every C r ∈ F n , M (C r ) ≥ F * . This leads to contradiction and therefore M is minimal.

Induction base: n = 0: the statement is satisfied vacuously.

Induction step: n = n 0 + 1: Every atom C r ∈ F n0+1 must occur in a head of a rule in P . such that {C 1 , . . . , C r−1 } ∩ N = ∅ and therefore {C 1 , . . . , C r } ⊆ F n0+1 . It follows then that M (C i ) = F * for 1 ≤ i ≤ r. By the construction of P M × , for every atom C r ∈ F n0+1 there must be a rule in P M × either of the form C r ← F * , A 1 , . . . , A m or of the form C r ← A 1 , . . . , A m . Moreover, since C r ∈ F n0+1 it follows that {A 1 , . . . , A m } ⊆ N ∪ F n0 . Therefore, by the induction hypothesis, M (A 1 , . . . , A m ) = M (A 1 , . . . , A m ) ≥ F * . Since M is also a model of P M × it must satisfy those rules thus M (C r ) ≥ F * . Case 2: N ⊂ N . We show that N is a model of P N leading to contradiction because, by definition, N is the minimum model of P N . Consider a rule R of the form C r ← A 1 , . . . , A m in P N . The rule R has been produced by a rule in P of the form:

If there exists A i ∈ N then also A i ∈ N and the rule is trivially satisfied by N . Assume, on the other hand, that {A 1 , . . . , A n } ⊆ N . It follows, by the definition of M , that M (A 1 , . . . , A m ) = T , M (C i ) = F * for i < r and M (C r ) = T . Therefore, there exist a rule in P M × of the form C r ← A 1 , . . . , A m . If M (A 1 , . . . , A m ) = F or M (A 1 , . . . , A m ) = F * then there exists A i ∈ N and N again satisfies the rule. If M (A 1 , . . . , A m ) = T then since M is a model of P M × it follows that M (C r ) = T . Since N is the collapse of M it is {A 1 , . . . , A m } ⊆ N and C r ∈ N . Therefore, N satisfies the rule R in P N .

The uniqueness of M follows directly from Proposition 3.

In order to establish Theorem 1, we show two lemmas (which essentially establish the left-to-right and the right-to-left directions of the theorem, respectively).

Let P be an LPOD program and let M be an answer set of P . Then, M is a -minimal model of P and M is solid.

Since M is an answer set of P , then, by Lemma 2, M is a model of P . Moreover, M is solid because our definition of answer sets does not involve the value T * . It remains to show that it is minimal with respect to the ordering. Assume, for the sake of contradiction, that there exists a model N of P with N ≺ M . By Lemma 4, M is (three-valued) -minimal. Therefore, N can not be solid. We first show that N can not be a model of the reduct P M × . Assume for the sake of contradiction that N is a model of P M × . We construct the following interpretation N :

We claim that N must also be a model of P M × . Consider first a rule of the form C ← F * , A 1 , . . . , A m . Since N is a model of P M × , it is N (C) ≥ F * . By the definition of N , it is N (C) ≥ F * and therefore N satisfies this rule. Consider now a rule of the form C ← A 1 , . . . , A m in P M × . We show that N also satisfies this rule. We perform a case analysis: Therefore, N must also be a model of P M × . Moreover, by definition, N is solid and N < M . This contradicts the fact that, by construction, M is the ≤-least model of P M × . In conclusion, N can not be a model of P M × . We now show that N can not be a model of P . As we showed above, N is not a model of P M × , and consequently there exists a rule in P M × that is not satisfied by N . Such a rule in P M × must have resulted due to a rule R of the following form in P :

According to the definition of P M × , for all i, 1 ≤ i ≤ k, M (not B i ) = T , and since N ≺ M , it is also N (not B i ) = T . Moreover, there exists some r ≤ n such that M (C 1 ) = · · · = M (C r−1 ) = F * and either r = n or M ( then N (A 1 , . . . , A m ) > F and N (C i ) = F . This implies that N (C 1 × · · · × C n ) = F and therefore N does not satisfy the rule R. If the rule that is not satisfied by N in P M × is of the form C r ← A 1 , . . . , A m , then N (C r ) < N (A 1 , . . . , A m ) and therefore, since N (C i ) ≤ F * for all i, 1 ≤ i ≤ r − 1, it is:

Thus, N is not a model of P .

Let P be an LPOD program and let M be a -minimal model of P and M is solid. Then, M is an answer set of P .

First observe that, by Lemma 3, M is also a model of P M × . We demonstrate that M is actually the ≤-least model of P M × . Assume, for the sake of contradiction, that N is the ≤-least model of P M × . Then, N will differ from M in some atoms A such that N (A) < M (A). We distinguish two cases. In the first case all the atoms A such that N (A) < M (A) have M (A) ≤ F * . In the second case there exist at least one atom A such that M (A) > F * .

In the first case it is easy to see that N ≺ M . We demonstrate that N is also model of P leading to contradiction since M is -minimal. Assume that N is not a model of P . Then, there exists in P a rule R of the form:

. . , A m ). We distinguish cases based on the value of N (A 1 , . . . , A m ):

Case 1: N (A 1 , . . . , A m ) = F . This case leads immediately to contradiction because N trivially satisfies R.

By the definition of the reduct, the rule C r ← A 1 , . . . , A m exists in P M × . Since N is a model of P M × , we get that N (C r ) > F . Moreover, N should also satisfy the rules C i ← F * , A 1 , . . . , A m for 1 ≤ i ≤ r − 1. Since N (C i ) ≤ M (C i ) and N (C r ) = M (C r ) we get N (C 1 ) = · · · = N (C r−1 ) = F * and N (C r ) = M (C r ). Therefore N (C 1 × · · · C n ) = M (C 1 × · · · C n ) and N (C 1 × · · · C n ) ≥ N (A 1 , . . . , A m ) (contradiction).

In the second case we construct the following interpretation N :

It is easy to see that N ≺ M . We demonstrate that N is a model of P , which will lead to a contradiction (since we have assumed that M is -minimal).

Assume N is not a model of P . Then, there exists in P a rule R of the form: Since M is a model of P , it is M (C 1 × · · · × C n ) ≥ F * . This implies that either M (C 1 ) = · · · = M (C n ) = F * or there exists r ≤ n such that M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) = T . By the definition of N , we get in both cases N (C 1 × · · · × C n ) ≥ F * (contradiction). Since M is a model of P , it is M (C 1 × · · · × C n ) = T . This implies that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) = T . By the definition of N , we get that N (C 1 × · · · × C n ) ≥ T * (contradiction). Since M is a model of P , it is M (C 1 × · · · × C n ) = T . This implies that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) = T . By the definition of the reduct, the rule C r ← A 1 , . . . , A m exists in P M × . Since N is a model of P M × , we get that N (C r ) = T . Thus, N (C 1 ) = · · · = N (C r−1 ) = F * and N (C r ) = T , and therefore N (C 1 × · · · × C n ) = T (contradiction).

Let P be an LPOD. Then, M is a three-valued answer set of P iff M is a consistent -minimal model of P and M is solid.

Immediate from Lemma 11 and Lemma 12.

Lemma 7 Let P be a consistent disjunctive extended logic program. Then, the answer sets of P according to Definition 20, coincide with the standard answer sets of P .

By taking n = 1 in Definition 19, we get the standard definition of reduct for consistent disjunctive extended logic programs.

Let P be a DLPOD program and let M be an answer set of P . Then, M is a model of P .

Consider any rule R in P of the form:

But then, the body of the rule R evaluates to F under M , and therefore M satisfies R. Consider now the case where R M × is nonempty and consists of the following rules:

We distinguish cases based on the value of M (A 1 , . . . , A m ): Case 2: M (A 1 , . . . , A m ) = F * . This implies that M (C r ) ≥ F * . We distinguish two subcases. If r = n then M (C 1 × · · · × C n ) = M (C 1 × · · · × C r ) ≥ F * because, by the definition of P M × it is M (C 1 ) = · · · = M (C r−1 ) = F * and we also know that M (C r ) ≥ F * . Thus, in this subcase M satisfies R. If r < n, then by the definition of P M × , M (C r ) = F * ; however, we know that M (C r ) ≥ F * , and thus M (C r ) = T . Thus, in this subcase M also satisfies R. × , M (C 1 ) = · · · = M (C r−1 ) = F * . This implies that M (C 1 × · · · × C n ) = T .

Let M be a model of a DLPOD P . Then, M is a model of P M × .

Consider any rule R in P of the form:

By the definition of P M × the following rules have been added to P M × :

where r is the least index such that M (C 1 ) = · · · = M (C r−1 ) = F * and either r = n or M (C r ) = F * . Obviously, the first r − 1 rules above are satisfied by M . For the rule C r ← A 1 , . . . , A m we distinguish two cases based on the value of M (A 1 , . . . , A m ). If M (A 1 , . . . , A m ) = F , then, the rule is trivially satisfied. If M (A 1 , . . . , A m ) > F , then, since rule R is satisfied by M and M (C r ) = F * , it has to be M (C r ) = T . Therefore, the rule C r ← A 1 , . . . , A m is satisfied by M .

Lemma 10 Every answer set M of a DLPOD P , is a -minimal model of P .

Assume there exists a model N of P with N M . We will show that N is also a model of P M × . Since N M , we also have N ≤ M . Since M is the ≤-least model of P M × , we will conclude that N = M .

Consider any rule R in P of the form:

Assume that R M × is nonempty. This means that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and either r = n or M (C r ) = F * . Then, R M × consists of the following rules:

C 1 ← F * , A 1 , . . . , A m · · · C r−1 ← F * , A 1 , . . . , A m C r ← A 1 , . . . , A m We show that N satisfies the above rules. We distinguish cases based on the value of M (A 1 , . . . , A m ): N (A 1 , . . . , A m ) ≤ F * . If  N (A 1 , . . . , A m ) = F then N trivially satisfies all the above rules. Assume therefore that N (A 1 , . . . , A m ) = F * . Recall now that M (C i ) = F * for all i, 1 ≤ i ≤ r − 1. Moreover, it has to be M (C r ) ≥ F * , because otherwise M would not satisfy the rule R. Since N M , it can only be N (C i ) = F * for all i, 1 ≤ i ≤ r − 1 and N (C r ) ≥ F * , because otherwise N would not be a model of P . Therefore, N satisfies the given rules of P M × . If N (A 1 , . . . , A m ) = F then N trivially satisfies all the above rules. Assume therefore that N (A 1 , . . . , A m ) = T . Recall now that M (C i ) = F * for all i, 1 ≤ i ≤ r − 1. Moreover, it has to be M (C r ) = T , because otherwise M would not satisfy the rule R. Since N M , it can only be N (C i ) = F * for all i, 1 ≤ i ≤ r − 1 and N (C r ) = T , because otherwise N would not be a model of P . Therefore, N satisfies the given rules of P M × .

Let P be a DLPOD. Then, M is an answer set of P iff M is a consistent -minimal model of P and M is solid.

The proof of the above theorem follows directly by the following two lemmas.

Let P be an DLPOD and let M be an answer set of P . Then, M is a consistent -minimal model of P and M is solid.

Since M is an answer set of P , then, by Lemma 8, M is a model of P . Moreover, M is solid because our definition of answer sets does not involve the value T * . It remains to show that it is minimal with respect to the ordering. Assume, for the sake of contradiction, that there exists a model N of P with N ≺ M . By Lemma 10, M is (three-valued) -minimal. Therefore, N can not be solid. We first show that N can not be a model of the reduct P M × . Assume for the sake of contradiction that N is a model of P M × . We construct the following interpretation N :

We claim that N must also be a model of P M × . Consider first a rule of the form C ← F * , A 1 , . . . , A m . Since N is a model of P M × , it is N (C) ≥ F * . By the definition of N , it is N (C) ≥ F * and therefore N satisfies this rule. Consider now a rule of the form C ← A 1 , . . . , A m in P M × . We show that N also satisfies this rule. We perform a case analysis: Therefore, N must also be a model of P M × . Moreover, by definition, N is solid and N < M . This contradicts the fact that, by construction, M is the ≤-least model of P M × . In conclusion, N can not be a model of P M × . We now show that N can not be a model of P . As we showed above, N is not a model of P M × , and consequently there exists a rule in P M × that is not satisfied by N . Such a rule in P M × must have resulted due to a rule R of the following form in P : C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k According to the definition of P M × , for all i, 1 ≤ i ≤ k, M (not B i ) = T , and since N ≺ M , it is also N (not B i ) = T . Moreover, there exists some r ≤ n such that M (C 1 ) = · · · = M (C r−1 ) = F * and either r = n or M (C r ) = F * . Since N ≺ M , it is N (C i ) ≤ F * for all i, 1 ≤ i ≤ r − 1. Consider now the rule that is not satisfied by N in P M × . If it is of the form C i ← F * , A 1 , . . . , A m , i, 1 ≤ i ≤ r − 1, then N (A 1 , . . . , A m ) > F and N (C i ) = F . This implies that N (C 1 × · · · × C n ) = F and therefore N does not satisfy the rule R. If the rule that is not satisfied by N in P M × is of the form C r ← A 1 , . . . , A m , then N (C r ) < N (A 1 , . . . , A m ) and therefore, since N (C i ) ≤ F * for all i, 1 ≤ i ≤ r − 1, it is: N (C 1 × · · · × C n ) < N (A 1 , . . . , A m , not B 1 , . . . , not B k ) Thus, N is not a model of P .

Let P be an DLPOD and let M be a consistent -minimal model of P and M is solid. Then, M is an answer set of P .

First observe that, by Lemma 9, M is also a model of P M × . We demonstrate that M is actually the ≤-least model of P M × . Assume, for the sake of contradiction, that N is the ≤-least model of P M × . Then, N will differ from M in some atoms A such that N (A) < M (A). We distinguish two cases. In the first case all the atoms A such that N (A) < M (A) have M (A) ≤ F * . In the second case there exist at least one atom A such that M (A) > F * .

In the first case it is easy to see that N ≺ M . We demonstrate that N is also model of P leading to contradiction since M is -minimal. Assume that N is not a model of P . Then, there exists in P a rule R of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k such that N (C 1 × · · · × C n ) < N (A 1 , . . . , A m , not B 1 , . . . , not B k ). Notice that this implies that N (not B 1 , . . . , not B k ) = M (not B 1 , . . . , not B k ) = T . Therefore, N (C 1 × · · · × C n ) < N (A 1 , . . . , A m ). We distinguish cases based on the value of N (A 1 , . . . , A m ):

Case 1: N (A 1 , . . . , A m ) = F . This case leads immediately to contradiction because N trivially satisfies R. Since M is a model of P , it is M (C 1 × · · · × C n ) ≥ M (A 1 , . . . , A m ) > F . This implies that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) ≥ F * . By the definition of the reduct, the rule C r ← A 1 , . . . , A m exists in P M × . Since N is a model of P M × , we get that N (C r ) > F . Moreover, N should also satisfy the rules C i ← F * , A 1 , . . . , A m for 1 ≤ i ≤ r − 1. Since N (C i ) ≤ M (C i ) and N (C r ) = M (C r ) we get N (C 1 ) = · · · = N (C r−1 ) = F * and N (C r ) = M (C r ). Therefore N (C 1 × · · · C n ) = M (C 1 × · · · C n ) and N (C 1 × · · · C n ) ≥ N (A 1 , . . . , A m ) (contradiction).

In the second case we construct the following interpretation N :

It is easy to see that N ≺ M . We demonstrate that N is a model of P , which will lead to a contradiction (since we have assumed that M is -minimal).

Assume N is not a model of P . Then, there exists in P a rule R of the form:

C 1 × · · · × C n ← A 1 , . . . , A m , not B 1 , . . . , not B k such that N (C 1 ×· · ·×C n ) < N (A 1 , . . . , A m , not B 1 , . . . , not B k ). Notice that this implies that N (not B 1 , . . . , not B k ) = N (not B 1 , . . . , not B k ) = M (not B 1 , . . . , not B k ) = T . Therefore, N (C 1 × · · · × C n ) < N (A 1 , . . . , A m ). We distinguish cases based on the value of N (A 1 , . . . , A m ):

Case 1: N (A 1 , . . . , A m ) = F . This case leads immediately to contradiction because N trivially satisfies R.

Revisiting explicit negation in answer set programming

Cr-prolog with ordered disjunction

CEUR Workshop Proceedings

Logic programming with ordered disjunction

Qualitative choice logic

Logic programs with ordered disjunction

A logical characterisation of ordered disjunction

Notions of strong equivalence for logic programs with ordered disjunction

Classical negation in logic programs and disjunctive databases

Sitzungsbericht PreuBische Akademie der Wissenschaften Berlin, physikalisch-mathematische Klasse II

Towards logic programs with ordered and unordered disjunction

Strongly equivalent logic programs

Constructible falsity

A new logical characterisation of stable models and answer sets

The semantics of predicate logic as a programming language

A m ) = F * . Since M is a model of P , it is M (C 1 × · · · × C n ) ≥ F * . This implies that either M

A m ) = T . Since M is a model of P , it is M (C 1 × · · · × C n ) = T . This implies that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) = T . By the definition of N

A m ) = T . Since M is a model of P , it is M (C 1 × · · · × C n ) = T . This implies that there exists some r, 1 ≤ r ≤ n, such that M (C 1 ) = · · · = M (C r−1 ) = F * and M (C r ) = T

Since N is a model of P M × , we get that N (C r ) = T . Thus, N (C 1 ) = · · · = N (C r−1 ) = F * and N (C r ) = T , and therefore N (C 1 × · · · × C n ) = T (contradiction)

We would like to thank the three anonymous reviewers of our paper for their careful and insightful comments.This research is co-financed by Greece and the European Union (European Social Fund-ESF) through the Operational Programme "Human Resources Development, Education and Lifelong Learning 2014-2020" in the context of the project "Techniques for implementing qualitative preferences in deductive querying systems" (5048151).