Choice Logics are a tool to express and reason about preferences. A choice logic extends classical propositional logic by adding non-classical binary connectives which express a certain form of ordering over interpretations that satisfy the connective; examples in the literature are Qualitative Choice Logic (QCL) which introduces the concept of ordered disjunction and Conjunctive Choice Logic (CCL) where an ordered variant of conjunction has been proposed. These logics have in common that interpretations ascribe a natural number, called satisfaction degree, to formulas; the lower this satisfaction degree, the more preferable the interpretation. In this paper, we present a general framework to capture several such logics and show how choice logics de ned in our framework can be encoded using Answer Set Programming. (ASP).
In this paper, we will generalize QCL and CCL by de ning a framework for logics in which preferences can be expressed by extending propositional logic with additional non-classical connectives. A logic of this framework will be referred to as a choice logic (CL). For instance, our framework allows to combine QCL and CCL into a new logic in a straightforward way. We provide some preliminary results for general CLs in terms of equivalence. The main contribution of the paper, however, is to encode choice logics from our framework by means of Answer Set Programming (ASP).
While there is a signi cant amount of literature on adding preferences to
core ASP (see, e.g. [
We brie y summarize the de nitions of the two choice logics that motivate our
general framework, namely QCL, introduced by Brewka et al. [
QCL is an extension of propositional logic that adds a new connective .
2. if F 2 FQCL, then (:F ) 2 FQCL;
2 f^; _; g.
Observe that every classical propositional formula is also a QCL-formula.
The semantics of QCL is based on satisfaction degrees. Interpretations ascribe a natural number to formulas. The lower this number (satisfaction degree) is, the more preferable this interpretation is for that particular formula. Before we can de ne the inference relation for satisfaction degrees, we need the concept of optionality, which expresses the number of satisfaction degrees that a formula can possibly have. #
mulas. Then the optionality of a QCL formula is de ned as follows: 1. opt(F ) = 1 if either F = x or F = :G; 2. opt(F # G) = max(opt(F ); opt(G)) for 3. opt(F G) = opt(F ) + opt(G). 2 f^; _g;
Now we can de ne the notion of satisfaction degree.1
1 Alternative satisfaction relatio#ns for QCL formulas have been proposed in [
We observe that the satisfaction degree of a formula under a given interpretation is unique. If there is a k 2 N such that I j kQCL F , we say that I satis es F with a degree of k. Otherwise, we say that F is n#ot satis ed under I. As an example, let us consider the formula F = ((x ^ y) x). Intuitively, F expresses that it is preferable to satisfy both x and y. If this is not possible, then it is still acceptable to satisfy only x. Formally, this means fx; yg j 1QCL F and fxg j 2QCL F , but ; j Q1CL F .
Since the purpose of QCL is to express preference, we are often interested in those models that satisfy a formula with minimal satisfaction degree, i.e. we are interested in the preferred models of a formula.
a preferred model of F if I j kQCL F with k 6= 1 and for all other interpretations J we have J j QmCL F with k m.
No#w let us cons#ider CCL. Syntactically, QCL and CCL are equivalent, but we write instead of for the choice connective. The semantics of CCL only di ers in the de nition of the satisfaction degree of the choice connective. That means, the optionality of a formula in CCL is de ned the same way as in QCL and the inference relation for the classical connectives remains unchanged between CCL and QCL. The semantics of the choice connective is as follows: De nition 5. Let I be an interpretation and let F# and G be CCL formulas.
8>m if I j 1CCL F and I j CmCL G k = <m + opt(G) if I j CmCL F , m 6= 1, and m 6= 1 :>1 otherwise
#
The intuitive meaning of a formula A B is that A and B is the most preferred outcome but, if that is not possible, only A is also acceptable but less preferred. 3
QCL and CCL are two logics that only di er in the de nition of the semantics of the choice operator. Furthermore, the choice operators considered in QCL and
CCL are not the only sensible choice operators. Consider, for example a choice connective that expresses that one prefers A to B but satisfying both or neither is not acceptable. This connective can express preferences between options that can not be chosen together, for example events at the same time slot. Therefore, we propose a general framework for choice logics (CL) that captures QCL and CCL and can also express other interesting choice connectives.
Syntactically, our framework closely resembles QCL and CCL, with the main di erence that we allow, in general, arbitrary many choice connectives. De nition 6. The set of choice connectives CL of a choice logic L is a nite set of binary connectives such that CL \ f:; ^; _g = ;. The set FL of formulas of a choice logic L is de ned inductively as follows:
2. if F 2 FL, then (:F ) 2 FL; 3. if F; G 2 FL, then (F G) 2 FL for #
2 f^; _g [ CL.
For CQCL = f g we retrieve the syntax of QCL and for CL = fg we retrieve the syntax of propositional logic.
For any choice logic, the semantics of the classical connectives for optionality and satisfaction degree are the same as for QCL and CCL. The semantics of a choice connective depends on the intended meaning of the connective. However, we can give reasonable restrictions for the semantics of choice connectives, for example the following upper bound for the optionality of a choice connective: optL(F
G)
(optL(F ) + 1) (optL(G) + 1): The idea is that F can have at most optL(F ) many nite satisfaction degrees, plus the in nite degree 1, i.e. there are at most optL(F ) + 1 degrees for F . Analogously for G. Thus, there are (optL(F ) + 1) (optL(G) + 1) possible combinations for how satisfaction degrees can be ascribed to (F G). In addition to giving an upper bound, we can also give the following lower bound: optL(F
G)
max(optL(F ); optL(G)): A choice connective should introduce new ways to distinguish between interpretations, or at least not give less options for doing so.
Lastly, for any reasonable choice connectives, the optionality of (F G) should only depend on the optionality of F and G. No other factors, such as the structure of F or G, should have an in uence.
a choice logic L. Then the optionality of an L-formula is given by the function optL : FL ! N such that 1. optL(F ) = 1 if either F = x or F = :G; 2. optL(F G) = max(optL(F ); optL(G)) for
2 CL there is a function f : N2 ! N such that
We are now ready to de ne the notion of satisfaction degrees for an arbitrary choice logic. For the semantics of choice connectives, we impose two crucial restrictions. Firstly, the satisfaction degree of a formula under any given interpretation should never be bigger than its optionality, unless the degree is 1. After all, the purpose of optionality is to assert the number of satisfaction degrees that a formula can possibly have. Secondly, the satisfaction degree of a formula F G under any given interpretation should only depend on the optionalities and satisfaction degrees of F and G. The structure of the formula or interpretation should have no impact on the satisfaction degree. For example, whether an interpretation assigns an even or uneven number of propositional variables to true should have no in uence on the satisfaction degree.
Therefore, the satisfaction degrees in a choice logic are de ned as follows. To simplify notation, we write degL(I; F ) = k if I j kL F holds.
tional variable, and F and G be L-formulas. Then the satisfaction degree of an L-formula under I is de ned as 1. I j kL x with k = 1 if x 2 I and k = 1 otherwise: 2. I j kL :F with k = 1 if I j L1 F and k = 1 otherwise; 3. I j kL F ^ G with k = max(m; n) if I j Lm F and I j nL G; 4. I j kL F _ G with k = min(m; n) if I j Lm F and I j nL G; 5. for every 2 CL there is a function g : (N [ f1g)4 ! (N [ f1g) such that degL(I; F
G) = g(optL(F ); optL(G); degL(I; F ); degL(I; G)) with degL(I; F
G) optL(F
G) or degL(I; F
G) = 1.
As before, we say that I satis es F with a degree of k. If I satis es F with a nite degree, then I is called a model of F . Furthermore, we can de ne preferred models analogously to QCL.
logic L. Then I is a preferred model of F , written as I 2 M odL(F ), if degL(I; F ) 6=
3.1
Examples for Choice Logics A CL is characterized by its choice connectives and by the meaning ascribed to said connectives. We have already seen the de nition of QCL and CCL and it is evident that they can be exp# ressed within our framework. As discussed above, we would like a connective that expresses the following situation: It is preferable to satisfy F ; if this is not possible, then G should be satis ed, but it is not acceptable to satisfy both F a#nd G. This connective is based on exclusive disjunction (XOR), similar to how is based on regular disjunction. We name this connective ordered exclusive disjunction, and call the corresponding choice logic Exclusive Disjunctive Choice Logic (XCL). # De nition 10. XCL is the choice logic such that CXCL = f g, # optXCL(F
G) = optXCL(F ) + optXCL(G); and degXCL(I; F
G) =
degXCL(I; G) + optXCL(F ) if degXCL(I; F ) = 1 # 8>degXCL(I; F ) > > > > > < > > > > > >:1 if degXCL(I; F ) < 1 and degXCL(I; G) = 1 and degXCL(I; G) < 1 otherwise #
We note that this connective can also be expressed in QCL as ((F G) ^ :(F ^ G)). But if this type of preference has to be expressed often in a given system, then a dedicated choice connective can simplify speci cations. Other, simple, choice connectives can not directly be expressed in QCL, for example because they ignore the optionality of a formula.
De nition 11. L1 is the choice logic such that CL1 = f g, optL1 (F
G) = optL1 (F ) + 1; and 8>degL1 (I; F ) < > :1 degL1 (I; F
G) = degL1 (I; F ) + 1 if degL1 (I; F ) < 1 and degL1 (I; G) = 1 if degL1 (I; F ) < 1 and degL1 (I; G) < 1 otherwise
The idea behind F G in L1 is that it is preferable to satisfy both F and G. If this is not possible, at least F should be satis ed. In this sense, the choice connective of L1 ful lls the same purpose as ordered conjunction in CCL. However, L1 does not use optionality to penalize less preferable interpretations. Instead, the degree of such interpretations is simply incremented by 1.
The framework also allows for CLs with multiple choice connectives. For example, one could de ne a CL that combines the choice connectives of QCL and CCL. # # De nition 12. QCCL is the choice logic such that CQCCL = f ; g, # # optQCCL(F optQCCL(F degQCCL(I; F degQCCL(I; F # # #
G) = optQCL(F G) = optCCL(F
# G) = degQCL(I; F G) = degCCL(I; F
G); G); # #
G); and
Since our framework is not very restrictive, there are in nitely many CLs. This includes more exotic CLs than the ones we have seen, with less intuitive properties. 3.2
Equivalence of formulas An important question in any logic is, when are two formulas equivalent. There are di erent ways to formalize equivalence between two choice formulas. The weakest one is to say that F and G are equivalent if they have the same preferred models, i.e. if M odL(F ) = M odL(G). A stronger notion would be the following.
degree-equivalent, written as F dL G, if for all interpretations I we have that degL(I; F ) = degL(I; G).
It is easy to see that degree-equivalence of two formulas implies that they
also have the same preferred models. However, degree-equivalence does not imply
that two formulas can be used interchangeably. This property is usually called
strong equivalence [
strongly equivalent, written as A sL B, if M odL(F ) = M odL(F [A=B]) for all
In general, two formulas that are degree-equivalent are not necessarily strongly equivalent. However, for some logics, like L1, it can be checked that degreeequivalence and strong equivalence coincide. We can show that the two concepts coincide for logics that completely ignore the optionality of formulas.
it holds that if degL(I; F ) = degL(I; F 0) and degL(I; G) = degL(I; G0), then degL(I; F G) = degL(I; F 0 G0).
A dL B. sL B i Proof. Assume rst that A dL B. By the de nition of a choice logic, the satisfaction degree of a formula only depends on the satisfaction degree and the optionality of its subformulas. Now, if a logic is optionality ignoring, then the satisfaction degree of a formula only depends on the satisfaction degree of its subformulas. Therefore, A dL B implies F dL F [A=B] and hence A sL B.
Assume now that A 6 dL B. We want to show that A 6 sL B, i.e. that there is a formula F such that M odL(F ) 6= M odL(F [A=B]).
Since A 6 dL B, there exists an interpretation I such that I j=Lm A and I j=nL B with m 6= n. Let k = min(m; n). We claim that there is a formula G such that the minimum degree that I satis es G is k. Assume k = m. Then the following formula has the desired property.
A ^ ^ x ^ x2var(A)nI :x :
A similar construction works in the case that k = n. By renaming the variables, we can assume that there are formulas G and H and interpretations IG, IH such that IG j=kL G, IH j=kL H, J 6j=lL G; H for any interpretation J and l < k, and G and H are variable disjoint from each other as well as from A and B. Additionally, we can assume that I \ IG = ;, I \ IH = ;, and IG \ IH = ;. We now construct
F = (A ^ G) _ (x ^ H); where x is a fresh variable. Observe that the minimal degree with which F (or F [A=B]) can possibly be satis ed is k, as either G or H need to be satis ed. Furthermore, IH [ fxg j=kL F and IH [ fxg j=kL F [A=B]. This means that any preferred model of F must satisfy F with a degree of k. The same is true for preferred models of F [A=B]. Also observe that since x is not contained in I or IG the model I [ IG does not satisfy (x ^ H).
Assume k = m. Then I j=kL A, and therefore I [ IG j=kL (A ^ G). Thus, I [ IG j=kL F , i.e. I [ IG 2 M odL(F ). Analogously, since I j=nL B, we have that I [ IG j=nL (B ^ G). Therefore I [ IG j=nL F [A=B]. Since n > k, we have I [ IG 62 M odL(F [A=B]). The case k = n is similar. tu
In order to guarantee strong equivalence for every choice logic, both the optionality and the satisfaction degree of two formulas must be the same.
optL(G), hold, then A sL B. dL B and optL(F ) =
Clearly, the reverse of Observation 2 is not always true, as Theorem 1 shows. However, for some logics, for example QCL and QCCL, it can be shown that the reverse holds, i.e. two formulas are strongly equivalent if and only if they are degree equivalent and have the same optionality. 4
We will provide a system written in Clingo 5 with which arbitrary choice logics can be encoded easily. Given a formula as input, each answer set of the encoding (composed of Listings 2{6 below) reports an interpretation together with its satisfaction degree. If one wishes to encode a CL that is not implemented in this system yet, then it su ces to specify the semantics of the CL's choice connectives in Listing 5. All other functionalities, such as syntax and the semantics of the classical connectives are xed and readily provided by the encoding. Based on this core encoding, other problems such as nding preferred models or checking for equivalence are then presented in Listings 7, 8, and 10.
Input formulas will be contained in the predicate inputformula/1. Classical connectives are represented by functions neg/1, and/2, as well as or/2. Choice connectives can be described with the function pref/3. The rst argument of pref/3 is a string that tells us which choice co#nnective #we are dealing with. For example, Listing 1 shows the encoding of ((a b) _ (:a c)).
Listing 1. input.lp 1 i n p u t f o r m u l a ( 2 or ( p r e f ( ' qcl ' , a , b ) , p r e f ( ' c c l ' , neg ( a ) , c ) ) 3 ) .
Encoding choice connectives as ternary functions allows for adding new choice connectives and specifying their semantics without worrying about the syntactic implications of doing so. To process the input formula syntactically, we dissect it into subformulas and atoms.
Listing 2. base.lp, Part 1 1 subformula (F , F) : i n p u t f o r m u l a (F ) . 2 subformula (F ,G) : subformula (F , neg (G) ) . 3 subformula (F ,G) : subformula (F , and (G, ) ) . 4 subformula (F ,G) : subformula (F , and ( ,G) ) . 5 subformula (F ,G) : subformula (F , or (G, ) ) . 6 subformula (F ,G) : subformula (F , or ( ,G) ) . 7 subformula (F ,G) : subformula (F , p r e f ( ,G, ) ) . 8 subformula (F ,G) : subformula (F , p r e f ( , ,G) ) . 9 10 atom (F) : subformula ( , F) , F = neg ( ) . 11 atom (F) : subformula ( , F) , F = and ( , ) . 12 atom (F) : subformula ( , F) , F = or ( , ) . 13 atom (F) : subformula ( , F) , F = p r e f ( , , ) . 14 atom (F) : subformula ( , F) , not atom (F ) .
The above program will yield the fact atom(x) for every constant x that occurs in the input formula. We can use this to guess all relevant interpretations.
Listing 3. base.lp, Part 2 1 f i n (F) : atom (F ) g . 2 out (F) : atom (F) , not i n (F ) .
As for semantics, we will compute the optionality and satisfaction degree of every subformula, and therefore also of the input formula. In Listing 4, we can see how this can be done for the classical connectives. Note that we use the constant #sup, which is built into Clingo, for 1.
Listing 4. base.lp, Part 3 1 opt (F , 1 ) : subformula ( , F) , atom (F ) . 2 opt (F , 1 ) : subformula ( , F) , F = neg ( ) . 3 opt (F ,X) : subformula ( , F) , F = and (G,H) , opt (G,X) , opt (H,Y) , 4 X >= Y. 5 opt (F ,Y) : subformula ( , F) , F = and (G,H) , opt (G,X) , opt (H,Y) , 6 X < Y. 7 opt (F ,X) : subformula ( , F) , F = or (G,H) , opt (G,X) , opt (H,Y) , 8 X >= Y. 9 opt (F ,Y) : subformula ( , F) , F = or (G,H) , opt (G,X) , opt (H,Y) , 10 X < Y. 11 12 deg (F , 1 ) : subformula ( , F) , atom (F) , i n (F ) . 13 deg (F,#sup ) : subformula ( , F) , atom (F) , out (F ) . 14 deg (F , 1 ) : subformula ( , F) , F = neg (G) , deg (G,#sup ) . 15 deg (F,#sup ) : subformula ( , F) , F = neg (G) , deg (G,K) , K < #sup . 16 deg (F ,X) : subformula ( , F) , F = and (G,H) , deg (G,X) , deg (H,Y) , 17 X >= Y. 18 deg (F ,Y) : subformula ( , F) , F = and (G,H) , deg (G,X) , deg (H,Y) , 19 X < Y. 20 deg (F ,X) : subformula ( , F) , F = or (G,H) , deg (G,X) , deg (H,Y) , 21 X < Y. 22 deg (F ,Y) : subformula ( , F) , F = or (G,H) , deg (G,X) , deg (H,Y) , 23 X >= Y.
To encode the semantics of the choice connectives, we will use the predicates optIn/3, optOut/4, degIn/5, and degOut/6. Recall that optL(F G) is a function over optL(F ) and optL(G). This function can be encoded via optIn/3 and optOut/4. The rst argument in both of these predicates is the string identifying which choice connective we are dealing with. The second and third arguments are the optionalities of F and G respectively. The fourth argument in optOut/4 is the result of the function call, i.e. the optionality of F G. The function for the satisfaction degree of the choice connective can be encoded analogously, except that degL(I; F G) is a function over optL(F ), degL(I; F ), optL(G), and degL(I; G). Listing 5 shows the speci cation of QCCL (cf. De nition 12).
Listing 5. qccl.lp 24 degIn ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 25 Deg1 > 1 , Deg1 < #sup . 26 degOut ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 , #sup ) : 27 degIn ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 28 Deg1 = #sup .
We can use this encoding of the optionality and degree functions to compute the values of opt/2 and deg/2 for the choice connectives. This ensures that the custom de ned choice connectives are integrated into the base system.
Listing 6. base.lp, Part 4 1 o p t I n (CL, X, Y) : subformula ( , F ) , F = p r e f (CL,G,H) , 2 opt (G,X) , opt (H,Y) . 3 opt (F , Z) : subformula ( , F ) , F = p r e f (CL,G,H) , 4 opt (G,X) , opt (H,Y) , optOut (CL, X, Y, Z ) . 5 6 degIn (CL, Opt1 , Deg1 , Opt2 , Deg2 ) : subformula ( , F ) , 7 F = p r e f (CL,G,H) , opt (G, Opt1 ) , opt (H, Opt2 ) , 8 deg (G, Deg1 ) , deg (H, Deg2 ) . 9 deg (F , Z) : subformula ( , F ) , F = p r e f (CL,G,H) , 10 opt (G, Opt1 ) , opt (H, Opt2 ) , deg (G, Deg1 ) , deg (H, Deg2 ) , 11 degOut (CL, Opt1 , Deg1 , Opt2 , Deg2 , Z ) .
4.1
Computing Preferred Models To compute all models of the input formula, one has to simply exclude those answer sets that result in an in nite satisfaction degree. Note that, for the sake of a cleaner output, we introduce a predicate deg/1, which holds the satisfaction degree of the input formula.
Listing 7. models.lp 1 deg (K) : i n p u t f o r m u l a (F ) , deg (F ,K) . 2 : deg(#sup ) . 3 #show i n / 1 . 4 #show deg / 1 .
Execute the following bash command to nd all models of a formula: $ c l i n g o base . l p q c c l . l p i n p u t . l p models . l p 0 Preferred models of the input formula can be computed with Clingo's #minimize statement. Instead of minimizing over deg/1, we minimize over the newly introduced predicate p/1, which only holds nite satisfaction degrees. This is simply to avoid warning messages, since the #minimize statement is not designed to work with #sup.
Listing 8. pref models.lp 1 deg (K) :
i n p u t f o r m u l a (F ) , deg (F ,K) . 2 : deg(#sup ) . 3 p (K) : deg (K) , K < #sup . 4 #minimize fX: p (X) g . 5 #show i n / 1 . 6 #show deg / 1 .
$ c l i n g o opt mode=optN
p r e f m o d e l s . l p This bash command gives the preferred model of the given formula: q u i e t =1 base . l p q c c l . l p i n p u t . l p 4.2
Checking for Equivalence Some problems, i.e. checking whether two formulas are equivalent, require more than one input formula. Recall, for example, that two QCL formulas are strongly equivalent if they are degree equivalent and have the same optionality (see Observation 2 and the remark following it). In what follows we discuss how to test strong equivalence in QCL using our encoding. We introduce the predicates inputfo#rm#ula1/1 and inputfor#mul#a2/1. In Listing 9, we see the encoding of F1 = (a (b c)) and F2 = ((a b) c). Note that F1 and F2 are strongly equivalent, since ordered disjunction is associative.
Listing 9. input2.lp 1 i n p u t f o r m u l a 1 ( 2 p r e f ( ' q c l ' , a , p r e f ( ' q c l ' , b , c ) ) 3 ) . 4 i n p u t f o r m u l a 2 ( 5 p r e f ( ' q c l ' , p r e f ( ' q c l ' , a , b ) , c ) 6 ) .
Instead of directly checking whether F1 and F2 are strongly equivalent, we solve the complementary problem: If we nd an interpretation (i.e. an answer set) where F1 and F2 are ascribed di erent satisfaction degrees, or show that the optionalities of F1 and F2 are not equal, then F1 and F2 are not strongly equivalent. See Listing 10 for how this can be implemented. The two input formulas are strongly equivalent if and only if the program is unsatis able.
Listing 10. strong equiv.lp 1 i n p u t f o r m u l a (F) : i n p u t f o r m u l a 1 (F ) . 2 i n p u t f o r m u l a (F) : i n p u t f o r m u l a 2 (F ) . 3 4 s a m e d e g r e e : i n p u t f o r m u l a 1 (F ) , i n p u t f o r m u l a 2 (G) , 5 deg (F ,K) , deg (G, L ) , K=L . 6 s a m e o p t i o n a l i t y : i n p u t f o r m u l a 1 (F ) , i n p u t f o r m u l a 2 (G) , 7 opt (F ,K) , opt (G, L ) , K=L . 8 : same degree , s a m e o p t i o n a l i t y . 9 10 #show i n / 1 . Note that Listing 10 also includes the rules inputformula(F) : inputformula1(F) and inputformula(F) : inputformula2(F). If this were not the case, then inputformula1/1 and inputformula2/1 could not be processed correctly by the base program. The following program call has to be made to check whether two formulas are degree-equivalent and have the same optionality: $ c l i n g o b a s e . l p q c c l . l p i n p u t . l p s t r o n g e q u i v . l p
To check directly for strong equivalence, instead of solving the complementary
problem, one could employ the saturation technique described by Egly et al. [
Of course, one could also check for degree-equivalence. This can be done analogously to Listing 10, except that we do not need to verify whether the two formulas have the same optionality or not. 5
In this paper, we introduced a framework for choice logics that encompasses both QCL and CCL. Furthermore, we showed how logics in this framework can be encoded via ASP, and how certain problems, such as nding preferred models for a given formula, or checking whether two formulas are strongly equivalent, can be solved using this encoding.
The encodings as provided in this paper are available under
There we also provide speci cations for further variants of choice logics.
The described ASP system can also be used in conjunction with other systems. As an alternative to encoding the choice connectives of a CL in pure ASP, the optionality- and degree functions could be described externally. For example, in Clingo 5, Python or Lua can be used to encode functions. Specifying the semantics of a CL in this way might be more convenient for some users. Furthermore, it is possible to make calls to Clingo 5 programs from other environments, such as Python. This allows for a system in which the business logic runs in Python, but when reasoning about preferences is needed, the ASP program can be employed.
A further possible eld of study is to investigate the CL framework more closely, by looking at some of the properties of choice logics. Since the de nition of a CL is not very restrictive, one could examine certain subgroups of choice logics that exhibit certain, possibly desirable, properties.
Lastly, instead of encoding choice logics within ASP, it would also be possible
to extend ASP itself by choice connectives. This has already been done with
ordered disjunction, resulting in Logic Programming with Ordered Disjunction
(LPOD) [