Introduction

Preferences are of interest in many areas of research such as economics, psychology, philosophy, but also computer science. Artificial intelligence, databases, and other fields are often concerned with analyzing "human choice behavior" [13].

One formal framework in which preferences can be expressed is Qualitative Choice Logic (QCL) [4]. QCL extends classical propositional logic by a binary connective #» ×, called ordered disjunction. Let F and G be formulas. Then the intuitive meaning of F #» ×G is that if possible, F should be satisfied. If this is not possible, then it is still acceptable, but less preferable, to satisfy only G. Satisfying neither F or G is not acceptable. More specifically, the satisfaction relation of QCL ascribes a natural number (called satisfaction degree) to a formula, given some interpretation. We prefer those interpretations that result in the smallest satisfaction degree for a formula. A further logic based on ordered connectives, called Conjunctive Choice Logic (CCL), has later been introduced in [2]. CCL replaces the ordered disjunction of QCL by another binary connective #» , called ordered conjunction. The intuitive meaning of F #» G is that if possible, F and G should be satisfied. If this is not possible, then at least F should be satisfied.

In this paper, we will generalize QCL and CCL by defining 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 significant amount of literature on adding preferences to core ASP (see, e.g. [6,5,9]), only a few papers encoded fundamental preference mechanisms in (standard) ASP. Work in this direction includes, for instance, encodings for the voting domain [7,12], and a translation from ASP with Resources (RASP) to plain ASP [8]. In fact, we opted here also for encodings in standard ASP, since our general framework of choice logics allows for connectives that can be quite different to concrete ASP add-ons.

Introducing QCL and CCL

We briefly summarize the definitions of the two choice logics that motivate our general framework, namely QCL, introduced by Brewka et al. [4], and CCL, introduced by Boudjelida and Benferhat [2]. In their original papers, both logics use slightly different notation for the same concepts. For the sake of uniformity, we stick to one notation that is a mixture of the notation of both papers.

QCL is an extension of propositional logic that adds a new connective #» ×.

Definition 1. The set of QCL-formulas F QCL is defined inductively as follows:

1. x ∈ F QCL , where x is a propositional variable;

2. if F ∈ F QCL , then (¬F ) ∈ F QCL ; 3. if F, G ∈ F QCL , then (F • G) ∈ F QCL for • ∈ {∧, ∨, #» ×}.

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 define 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. Definition 2. Let x be a propositional variable, and let F and G be QCL formulas. Then the optionality of a QCL formula is defined 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).

Now we can define the notion of satisfaction degree. 1 Definition 3. Let I be an interpretation, x be a propositional variable, and F and G be QCL formulas. Then the satisfaction degree k ∈ N ∪ {∞} of a QCL formula under I is defined as follows:

1. I |∼ QCL k x with k = 1 if x ∈ I and k = ∞ otherwise; 2. I |∼ QCL k ¬F with k = 1 if I |∼ QCL ∞ F and k = ∞ otherwise; 3. I |∼ QCL k F ∧ G with k = max(m, n) for I |∼ QCL m F and I |∼ QCL n G: 4. I |∼ QCL k F ∨ G with k = min(m, n) for I |∼ QCL m F and I |∼ QCL n G; 5. I |∼ QCL k F #» ×G iff I |∼ QCL k F for k < ∞ or I |∼ QCL ∞ F, I |∼ QCL m G, and k = m + opt(F ).

We observe that the satisfaction degree of a formula under a given interpretation is unique. If there is a k ∈ N such that I |∼ QCL k F , we say that I satisfies F with a degree of k. Otherwise, we say that F is not satisfied 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 {x, y}

|∼ QCL 1 F and {x} |∼ QCL 2 F , but ∅ |∼ QCL ∞ 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.

k =      m if I |∼ CCL 1 F and I |∼ CCL m G m + opt(G) if I |∼ CCL m F , m = 1, and m = ∞ ∞ 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.

A Framework for Choice Logics

QCL and CCL are two logics that only differ in the definition 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 difference that we allow, in general, arbitrary many choice connectives. Definition 6. The set of choice connectives C L of a choice logic L is a finite set of binary connectives such that C L ∩ {¬, ∧, ∨} = ∅. The set F L of formulas of a choice logic L is defined inductively as follows:

1. x ∈ F L , where x is a propositional variable; 2. if F ∈ F L , then (¬F ) ∈ F L ; 3. if F, G ∈ F L , then (F • G) ∈ F L for • ∈ {∧, ∨} ∪ C L . For C QCL = { #»

×} we retrieve the syntax of QCL and for C L = {} 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:

opt L (F • G) ≤ (opt L (F ) + 1) • (opt L (G) + 1).

The idea is that F can have at most opt L (F ) many finite satisfaction degrees, plus the infinite degree ∞, i.e. there are at most opt L (F ) + 1 degrees for F . Analogously for G. Thus, there are (opt L (F ) + 1) • (opt L (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:

opt L (F • G) ≥ max(opt L (F ), opt L (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 influence. Definition 7. Let x be a propositional variable, and let F and G be formulas of a choice logic L. Then the optionality of an L-formula is given by the function

opt L : F L → N such that 1. opt L (F ) = 1 if either F = x or F = ¬G; 2. opt L (F • G) = max(opt L (F ), opt L (G)) for • ∈ {∧, ∨}; 3. for every • ∈ C L there is a function f : N 2 → N such that opt L (F • G) = f (opt L (F ), opt L (G)) with max(opt L (F ), opt L (G)) ≤ opt L (F • G) ≤ (opt L (F ) + 1) • (opt L (G) + 1).

We are now ready to define 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 ∞. 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 influence on the satisfaction degree.

Therefore, the satisfaction degrees in a choice logic are defined as follows. To simplify notation, we write deg

L (I, F ) = k if I |∼ L k F holds.

Definition 8. Let L be a choice logic, I be an interpretation, x be a propositional variable, and F and G be L-formulas. Then the satisfaction degree of an L-formula under I is defined as

1. I |∼ L k x with k = 1 if x ∈ I and k = ∞ otherwise: 2. I |∼ L k ¬F with k = 1 if I |∼ L ∞ F and k = ∞ otherwise; 3. I |∼ L k F ∧ G with k = max(m, n) if I |∼ L m F and I |∼ L n G; 4. I |∼ L k F ∨ G with k = min(m, n) if I |∼ L m F and I |∼ L n G; 5. for every • ∈ C L there is a function g : (N ∪ {∞}) 4 → (N ∪ {∞}) such that deg L (I, F • G) = g(opt L (F ), opt L (G), deg L (I, F ), deg L (I, G)) with deg L (I, F • G) ≤ opt L (F • G) or deg L (I, F • G) = ∞.

As before, we say that I satisfies F with a degree of k. If I satisfies F with a finite degree, then I is called a model of F . Furthermore, we can define preferred models analogously to QCL. Definition 9. Let I be an interpretation and let F be a formula of some choice logic L. Then I is a preferred model of F , written as

I ∈ M od L (F ), if deg L (I, F ) =

∞ and for all other interpretations J we have deg L (I, F ) ≤ deg L (J , F ).

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 definition of QCL and CCL and it is evident that they can be expressed 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 satisfied, but it is not acceptable to satisfy both F and 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).

Definition 10. XCL is the choice logic such that

C XCL = { #» ⊕}, opt XCL (F #» ⊕G) = opt XCL (F ) + opt XCL (G),

and

deg XCL (I, F #» ⊕G) =                deg XCL (I, F ) if deg XCL (I, F ) < ∞ and deg XCL (I, G) = ∞ deg XCL (I, G) + opt XCL (F ) if deg XCL (I, F ) = ∞ and deg XCL (I, G) < ∞ ∞ 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 specifications. Other, simple, choice connectives can not directly be expressed in QCL, for example because they ignore the optionality of a formula.

Definition 11. L 1 is the choice logic such that C L1 = {•}, opt L1 (F • G) = opt L1 (F ) + 1,

and

deg L1 (I, F • G) =      deg L1 (I, F ) if deg L1 (I, F ) < ∞ and deg L1 (I, G) < ∞ deg L1 (I, F ) + 1 if deg L1 (I, F ) < ∞ and deg L1 (I, G) = ∞ ∞ otherwise

The idea behind F • G in L 1 is that it is preferable to satisfy both F and G. If this is not possible, at least F should be satisfied. In this sense, the choice connective of L 1 fulfills the same purpose as ordered conjunction in CCL. However, L 1 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 define a CL that combines the choice connectives of QCL and CCL.

Definition 12. QCCL is the choice logic such that

C QCCL = { #» ×, #» }, opt QCCL (F #» ×G) = opt QCL (F #» ×G), opt QCCL (F #» G) = opt CCL (F #» G), deg QCCL (I, F #» ×G) = deg QCL (I, F #» ×G),anddeg QCCL (I, F #» G) = deg CCL (I, F #» G).

Since our framework is not very restrictive, there are infinitely many CLs. This includes more exotic CLs than the ones we have seen, with less intuitive properties.

Equivalence of formulas

An important question in any logic is, when are two formulas equivalent. There are different 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 od L (F ) = M od L (G). A stronger notion would be the following. Definition 13. Let F and G be formulas of some choice logic L. F and G are degree-equivalent, written as F ≡ L d G, if for all interpretations I we have that

deg L (I, F ) = deg L (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 [11]. Definition 14. Let A and B be formulas of some choice logic L. A and B are strongly equivalent, written as

A ≡ L s B, if M od L (F ) = M od L (F [A/B]) for all L-formulas F .

In general, two formulas that are degree-equivalent are not necessarily strongly equivalent. However, for some logics, like L 1 , 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.

A ≡ L s B iff A ≡ L d B. Proof. Assume first that A ≡ L d B.

By the definition 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 ≡ L d B implies F ≡ L d F [A/B] and hence A ≡ L s B. Assume now that A ≡ L d B.

We want to show that A ≡ L s B, i.e. that there is a formula

F such that M od L (F ) = M od L (F [A/B]).

Since A ≡ L d B, there exists an interpretation I such that I |= L m A and

I |= L n B with m = n. Let k = min(m, n).

We claim that there is a formula G such that the minimum degree that I satisfies G is k. Assume k = m. Then the following formula has the desired property.

A ∧ x∈I x ∧ x∈var(A)\I ¬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

I G , I H such that I G |= L k G, I H |= L k H, J |= L l 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 ∩ I G = ∅, I ∩ I H = ∅, and I G ∩ I H = ∅. 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 satisfied is k, as either G or H need to be satisfied. Furthermore,

I H ∪ {x} |= L k F and I H ∪ {x} |= L k 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 I G the model I ∪ I G does not satisfy (x ∧ H).

Assume k = m. Then I |= L k A, and therefore

I ∪ I G |= L k (A ∧ G). Thus, I ∪ I G |= L k F , i.e. I ∪ I G ∈ M od L (F ). Analogously, since I |= L n B, we have that I ∪ I G |= L n (B ∧ G). Therefore I ∪ I G |= L n F [A/B]. Since n > k, we have I ∪ I G ∈ M od L (F [A/B]). The case k = n is similar.

In order to guarantee strong equivalence for every choice logic, both the optionality and the satisfaction degree of two formulas must be the same.

Observation 2 Let L be an arbitrary choice logic. If both, A ≡ L d B and opt L (F ) = opt L (G), hold, then A ≡ L s B.

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.

ASP Encoding

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 suffices 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 fixed and readily provided by the encoding. Based on this core encoding, other problems such as finding 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 first argument of pref/3 is a string that tells us which choice connective we are dealing with. For example, Listing 1 shows the encoding of ((a #» ×b) ∨ (¬a #» c)). 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.

To encode the semantics of the choice connectives, we will use the predicates optIn/3, optOut/4, degIn/5, and degOut/6. Recall that opt L (F • G) is a function over opt L (F ) and opt L (G). This function can be encoded via optIn/3 and optOut/4. The first 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 deg o p t I n ( ' q c l ' , Opt1 , Opt2 ) , Z = Opt1 + Opt2 . 5 6 degOut ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 , Deg1 ) :− 7 degIn ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 8

L (I, F • G) is a function over opt L (F ), deg L (I, F ), opt L (G)

Deg1 < #sup . 9 degOut ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 , Deg2 + Opt1 ) :− 10 degIn ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 11 Deg1 = #sup , Deg2 < #sup . 12 degOut ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 , #sup ) :− 13 degIn ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 14 Deg1 = #sup , Deg2 = #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 defined choice connectives are integrated into the base system.

Computing Preferred Models

To compute all models of the input formula, one has to simply exclude those answer sets that result in an infinite 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. Execute the following bash command to find all models of a formula:

$ 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 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 finite satisfaction degrees. This is simply to avoid warning messages, since the #minimize statement is not designed to work with #sup. This bash command gives the preferred model of the given formula:

$ c l i n g o −−opt−mode=optN −−q u i e t =1 b a s e . l p q c c l . l p i n p u t . l p p r e f m o d e l s . l p

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 inputformula1/1 and inputformula2/1. In Listing 9, we see the encoding of

F 1 = (a #» ×(b #» ×c)) and F 2 = ((a #» ×b) #» ×c).

Note that F 1 and F 2 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 ( 2p 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 F 1 and F 2 are strongly equivalent, we solve the complementary problem: If we find an interpretation (i.e. an answer set) where F 1 and F 2 are ascribed different satisfaction degrees, or show that the optionalities of F 1 and F 2 are not equal, then F 1 and F 2 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 unsatisfiable. Note that Listing 10 also includes the rules inputformula(F) :− inputformula1(F) and inputformula(F) :− inputformula2(F). If this were not the case, then input-formula1/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. [10]. This would require modifications to the base program, as default negation can not be used with this technique.

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.

Conclusion

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 finding 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 https://github.com/mbernr/choice-logics-asp.

There we also provide specifications 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 field of study is to investigate the CL framework more closely, by looking at some of the properties of choice logics. Since the definition 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) [3,6].